helm/software/matita/contribs/procedural/CoRN/ftc/FunctSequence.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "CoRN.ma".
  18
  19 (* $Id: FunctSequence.v,v 1.5 2004/04/23 10:00:58 lcf Exp $ *)
  20
  21 include "ftc/Continuity.ma".
  22
  23 include "ftc/PartInterval.ma".
  24
  25 (* UNEXPORTED
  26 Section Definitions
  27 *)
  28
  29 (*#* *Sequences of Functions
  30
  31 In this file we define some more operators on functions, namely
  32 sequences and limits.  These concepts are defined only for continuous
  33 functions.
  34
  35 %\begin{convention}% Throughout this section:
  36  - [a] and [b] will be real numbers and the interval [[a,b]]
  37 will be denoted by [I];
  38  - [f, g] and [h] will denote sequences of continuous functions;
  39  - [F, G] and [H] will denote continuous functions.
  40
  41 %\end{convention}%
  42
  43 **Definitions
  44
  45 A sequence of functions is simply an object of type [nat->PartIR].
  46 However, we will be interested mostly in convergent and Cauchy
  47 sequences.  Several definitions of these concepts will be formalized;
  48 they mirror the several different ways in which a Cauchy sequence can
  49 be defined.  For a discussion on the different notions of convergent
  50 see Bishop 1967.
  51 *)
  52
  53 (* UNEXPORTED
  54 cic:/CoRN/ftc/FunctSequence/Definitions/a.var
  55 *)
  56
  57 (* UNEXPORTED
  58 cic:/CoRN/ftc/FunctSequence/Definitions/b.var
  59 *)
  60
  61 (* UNEXPORTED
  62 cic:/CoRN/ftc/FunctSequence/Definitions/Hab.var
  63 *)
  64
  65 (* begin hide *)
  66
  67 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/I.con" "Definitions__" as definition.
  68
  69 (* end hide *)
  70
  71 (* UNEXPORTED
  72 cic:/CoRN/ftc/FunctSequence/Definitions/f.var
  73 *)
  74
  75 (* UNEXPORTED
  76 cic:/CoRN/ftc/FunctSequence/Definitions/F.var
  77 *)
  78
  79 (* UNEXPORTED
  80 cic:/CoRN/ftc/FunctSequence/Definitions/contf.var
  81 *)
  82
  83 (* UNEXPORTED
  84 cic:/CoRN/ftc/FunctSequence/Definitions/contF.var
  85 *)
  86
  87 (* begin hide *)
  88
  89 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/incf.con" "Definitions__" as definition.
  90
  91 inline procedural "cic:/CoRN/ftc/FunctSequence/Definitions/incF.con" "Definitions__" as definition.
  92
  93 (* end hide *)
  94
  95 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq.con" as definition.
  96
  97 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'.con" as definition.
  98
  99 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq.con" as definition.
 100
 101 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1.con" as definition.
 102
 103 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'.con" as definition.
 104
 105 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2.con" as definition.
 106
 107 (*#*
 108 These definitions are all shown to be equivalent.
 109 *)
 110
 111 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq'.con" as lemma.
 112
 113 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq.con" as lemma.
 114
 115 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq'.con" as lemma.
 116
 117 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq2.con" as lemma.
 118
 119 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_seq.con" as lemma.
 120
 121 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_norm.con" as lemma.
 122
 123 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_norm_seq.con" as lemma.
 124
 125 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq'.con" as lemma.
 126
 127 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_seq1.con" as lemma.
 128
 129 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_seq1.con" as lemma.
 130
 131 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_seq.con" as lemma.
 132
 133 (*#*
 134 A Cauchy sequence of functions is pointwise a Cauchy sequence.
 135 *)
 136
 137 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_real.con" as lemma.
 138
 139 (* UNEXPORTED
 140 End Definitions
 141 *)
 142
 143 (* UNEXPORTED
 144 Section More_Definitions
 145 *)
 146
 147 (* UNEXPORTED
 148 cic:/CoRN/ftc/FunctSequence/More_Definitions/a.var
 149 *)
 150
 151 (* UNEXPORTED
 152 cic:/CoRN/ftc/FunctSequence/More_Definitions/b.var
 153 *)
 154
 155 (* UNEXPORTED
 156 cic:/CoRN/ftc/FunctSequence/More_Definitions/Hab.var
 157 *)
 158
 159 (* begin hide *)
 160
 161 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Definitions/I.con" "More_Definitions__" as definition.
 162
 163 (* end hide *)
 164
 165 (* UNEXPORTED
 166 cic:/CoRN/ftc/FunctSequence/More_Definitions/f.var
 167 *)
 168
 169 (* UNEXPORTED
 170 cic:/CoRN/ftc/FunctSequence/More_Definitions/contf.var
 171 *)
 172
 173 (*#*
 174 We can also say that [f] is simply convergent if it converges to some
 175 continuous function.  Notice that we do not quantify directly over
 176 partial functions, for reasons which were already explained.
 177 *)
 178
 179 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq.con" as definition.
 180
 181 (*#*
 182 It is useful to extract the limit as a partial function:
 183 *)
 184
 185 (* begin show *)
 186
 187 (* UNEXPORTED
 188 cic:/CoRN/ftc/FunctSequence/More_Definitions/H.var
 189 *)
 190
 191 (* end show *)
 192
 193 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_Lim.con" as definition.
 194
 195 (* UNEXPORTED
 196 End More_Definitions
 197 *)
 198
 199 (* UNEXPORTED
 200 Section Irrelevance_of_Proofs
 201 *)
 202
 203 (*#* **Irrelevance of Proofs
 204
 205 This section contains a number of technical results stating mainly that being a Cauchy sequence or converging to some limit is a property of the sequence itself and independent of the proofs we supply of its continuity or the continuity of its limit.
 206 *)
 207
 208 (* UNEXPORTED
 209 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/a.var
 210 *)
 211
 212 (* UNEXPORTED
 213 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/b.var
 214 *)
 215
 216 (* UNEXPORTED
 217 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/Hab.var
 218 *)
 219
 220 (* begin hide *)
 221
 222 inline procedural "cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/I.con" "Irrelevance_of_Proofs__" as definition.
 223
 224 (* end hide *)
 225
 226 (* UNEXPORTED
 227 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/f.var
 228 *)
 229
 230 (* begin show *)
 231
 232 (* UNEXPORTED
 233 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf.var
 234 *)
 235
 236 (* UNEXPORTED
 237 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contf0.var
 238 *)
 239
 240 (* end show *)
 241
 242 (* UNEXPORTED
 243 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/F.var
 244 *)
 245
 246 (* begin show *)
 247
 248 (* UNEXPORTED
 249 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF.var
 250 *)
 251
 252 (* UNEXPORTED
 253 cic:/CoRN/ftc/FunctSequence/Irrelevance_of_Proofs/contF0.var
 254 *)
 255
 256 (* end show *)
 257
 258 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wd.con" as lemma.
 259
 260 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq'_wd.con" as lemma.
 261
 262 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq2_wd.con" as lemma.
 263
 264 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_norm_fun_seq_wd.con" as lemma.
 265
 266 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq1_wd.con" as lemma.
 267
 268 (* UNEXPORTED
 269 End Irrelevance_of_Proofs
 270 *)
 271
 272 (* UNEXPORTED
 273 Section More_Proof_Irrelevance
 274 *)
 275
 276 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq_wd.con" as lemma.
 277
 278 (* UNEXPORTED
 279 End More_Proof_Irrelevance
 280 *)
 281
 282 (* UNEXPORTED
 283 Section More_Properties
 284 *)
 285
 286 (*#* **Other Properties
 287
 288 Still more technical details---a convergent sequence converges to its
 289 limit; the limit is a continuous function; and convergence is well
 290 defined with respect to functional equality in the interval [[a,b]].
 291 *)
 292
 293 (* UNEXPORTED
 294 cic:/CoRN/ftc/FunctSequence/More_Properties/a.var
 295 *)
 296
 297 (* UNEXPORTED
 298 cic:/CoRN/ftc/FunctSequence/More_Properties/b.var
 299 *)
 300
 301 (* UNEXPORTED
 302 cic:/CoRN/ftc/FunctSequence/More_Properties/Hab.var
 303 *)
 304
 305 (* begin hide *)
 306
 307 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Properties/I.con" "More_Properties__" as definition.
 308
 309 (* end hide *)
 310
 311 (* UNEXPORTED
 312 cic:/CoRN/ftc/FunctSequence/More_Properties/f.var
 313 *)
 314
 315 (* UNEXPORTED
 316 cic:/CoRN/ftc/FunctSequence/More_Properties/g.var
 317 *)
 318
 319 (* begin show *)
 320
 321 (* UNEXPORTED
 322 cic:/CoRN/ftc/FunctSequence/More_Properties/contf.var
 323 *)
 324
 325 (* UNEXPORTED
 326 cic:/CoRN/ftc/FunctSequence/More_Properties/contf0.var
 327 *)
 328
 329 (* UNEXPORTED
 330 cic:/CoRN/ftc/FunctSequence/More_Properties/contg.var
 331 *)
 332
 333 (* UNEXPORTED
 334 cic:/CoRN/ftc/FunctSequence/More_Properties/contg0.var
 335 *)
 336
 337 (* end show *)
 338
 339 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq'.con" as lemma.
 340
 341 (* UNEXPORTED
 342 cic:/CoRN/ftc/FunctSequence/More_Properties/F.var
 343 *)
 344
 345 (* UNEXPORTED
 346 cic:/CoRN/ftc/FunctSequence/More_Properties/G.var
 347 *)
 348
 349 (* begin show *)
 350
 351 (* UNEXPORTED
 352 cic:/CoRN/ftc/FunctSequence/More_Properties/contF.var
 353 *)
 354
 355 (* UNEXPORTED
 356 cic:/CoRN/ftc/FunctSequence/More_Properties/contF0.var
 357 *)
 358
 359 (* UNEXPORTED
 360 cic:/CoRN/ftc/FunctSequence/More_Properties/contG.var
 361 *)
 362
 363 (* UNEXPORTED
 364 cic:/CoRN/ftc/FunctSequence/More_Properties/contG0.var
 365 *)
 366
 367 (* end show *)
 368
 369 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl.con" as lemma.
 370
 371 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr.con" as lemma.
 372
 373 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdl'.con" as lemma.
 374
 375 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_fun_seq'_wdr'.con" as lemma.
 376
 377 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_fun_seq_wd.con" as lemma.
 378
 379 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_cont_Lim.con" as lemma.
 380
 381 inline procedural "cic:/CoRN/ftc/FunctSequence/Cauchy_conv_fun_seq.con" as lemma.
 382
 383 inline procedural "cic:/CoRN/ftc/FunctSequence/conv_Cauchy_fun_seq.con" as lemma.
 384
 385 (*#*
 386 More interesting is the fact that a convergent sequence of functions converges pointwise as a sequence of real numbers.
 387 *)
 388
 389 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_conv_imp_seq_conv.con" as lemma.
 390
 391 (*#*
 392 And a sequence of real numbers converges iff the corresponding sequence of constant functions converges to the corresponding constant function.
 393 *)
 394
 395 inline procedural "cic:/CoRN/ftc/FunctSequence/seq_conv_imp_fun_conv.con" as lemma.
 396
 397 (* UNEXPORTED
 398 End More_Properties
 399 *)
 400
 401 (* UNEXPORTED
 402 Hint Resolve Cauchy_cont_Lim: continuous.
 403 *)
 404
 405 (* UNEXPORTED
 406 Section Algebraic_Properties
 407 *)
 408
 409 (*#* **Algebraic Properties
 410
 411 We now study how convergence is affected by algebraic operations, and some algebraic properties of the limit function.
 412 *)
 413
 414 (* UNEXPORTED
 415 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/a.var
 416 *)
 417
 418 (* UNEXPORTED
 419 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/b.var
 420 *)
 421
 422 (* UNEXPORTED
 423 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/Hab.var
 424 *)
 425
 426 (* begin hide *)
 427
 428 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/I.con" "Algebraic_Properties__" as definition.
 429
 430 (* end hide *)
 431
 432 (* UNEXPORTED
 433 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/f.var
 434 *)
 435
 436 (* UNEXPORTED
 437 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/g.var
 438 *)
 439
 440 (* UNEXPORTED
 441 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contf.var
 442 *)
 443
 444 (* UNEXPORTED
 445 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contg.var
 446 *)
 447
 448 (*#*
 449 First, the limit function is unique.
 450 *)
 451
 452 inline procedural "cic:/CoRN/ftc/FunctSequence/FLim_unique.con" as lemma.
 453
 454 (*#* Constant sequences (not sequences of constant functions!) always converge.
 455 *)
 456
 457 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_const.con" as lemma.
 458
 459 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_const.con" as lemma.
 460
 461 (*#*
 462 We now prove that if two sequences converge than their sum (difference, product) also converge to the sum (difference, product) of their limits.
 463 *)
 464
 465 (* UNEXPORTED
 466 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/F.var
 467 *)
 468
 469 (* UNEXPORTED
 470 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/G.var
 471 *)
 472
 473 (* UNEXPORTED
 474 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contF.var
 475 *)
 476
 477 (* UNEXPORTED
 478 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/contG.var
 479 *)
 480
 481 (* begin show *)
 482
 483 (* UNEXPORTED
 484 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convF.var
 485 *)
 486
 487 (* UNEXPORTED
 488 cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/convG.var
 489 *)
 490
 491 (* end show *)
 492
 493 (* begin hide *)
 494
 495 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incf.con" "Algebraic_Properties__" as definition.
 496
 497 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incg.con" "Algebraic_Properties__" as definition.
 498
 499 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incF.con" "Algebraic_Properties__" as definition.
 500
 501 inline procedural "cic:/CoRN/ftc/FunctSequence/Algebraic_Properties/incG.con" "Algebraic_Properties__" as definition.
 502
 503 (* end hide *)
 504
 505 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus'.con" as lemma.
 506
 507 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus'.con" as lemma.
 508
 509 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult'.con" as lemma.
 510
 511 (* UNEXPORTED
 512 End Algebraic_Properties
 513 *)
 514
 515 (* UNEXPORTED
 516 Section More_Algebraic_Properties
 517 *)
 518
 519 (* UNEXPORTED
 520 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/a.var
 521 *)
 522
 523 (* UNEXPORTED
 524 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/b.var
 525 *)
 526
 527 (* UNEXPORTED
 528 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hab.var
 529 *)
 530
 531 (* begin hide *)
 532
 533 inline procedural "cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/I.con" "More_Algebraic_Properties__" as definition.
 534
 535 (* end hide *)
 536
 537 (* UNEXPORTED
 538 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/f.var
 539 *)
 540
 541 (* UNEXPORTED
 542 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/g.var
 543 *)
 544
 545 (* UNEXPORTED
 546 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contf.var
 547 *)
 548
 549 (* UNEXPORTED
 550 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/contg.var
 551 *)
 552
 553 (*#*
 554 The same is true if we don't make the limits explicit.
 555 *)
 556
 557 (* begin hide *)
 558
 559 (* UNEXPORTED
 560 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hf.var
 561 *)
 562
 563 (* UNEXPORTED
 564 cic:/CoRN/ftc/FunctSequence/More_Algebraic_Properties/Hg.var
 565 *)
 566
 567 (* end hide *)
 568
 569 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_plus.con" as lemma.
 570
 571 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_plus.con" as lemma.
 572
 573 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_minus.con" as lemma.
 574
 575 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_minus.con" as lemma.
 576
 577 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_mult.con" as lemma.
 578
 579 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_mult.con" as lemma.
 580
 581 (* UNEXPORTED
 582 End More_Algebraic_Properties
 583 *)
 584
 585 (* UNEXPORTED
 586 Section Still_More_Algebraic_Properties
 587 *)
 588
 589 (* UNEXPORTED
 590 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/a.var
 591 *)
 592
 593 (* UNEXPORTED
 594 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/b.var
 595 *)
 596
 597 (* UNEXPORTED
 598 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hab.var
 599 *)
 600
 601 (* begin hide *)
 602
 603 inline procedural "cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/I.con" "Still_More_Algebraic_Properties__" as definition.
 604
 605 (* end hide *)
 606
 607 (* UNEXPORTED
 608 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/f.var
 609 *)
 610
 611 (* UNEXPORTED
 612 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/contf.var
 613 *)
 614
 615 (* UNEXPORTED
 616 cic:/CoRN/ftc/FunctSequence/Still_More_Algebraic_Properties/Hf.var
 617 *)
 618
 619 (*#*
 620 As a corollary, we get the analogous property for the sequence of algebraic inverse functions.
 621 *)
 622
 623 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Lim_seq_inv.con" as lemma.
 624
 625 inline procedural "cic:/CoRN/ftc/FunctSequence/fun_Cauchy_prop_inv.con" as lemma.
 626
 627 (* UNEXPORTED
 628 End Still_More_Algebraic_Properties
 629 *)
 630
 631 (* UNEXPORTED
 632 Hint Resolve Continuous_I_Sum Continuous_I_Sumx Continuous_I_Sum0: continuous.
 633 *)
 634