helm/software/matita/contribs/CoRN-Procedural/ftc/MoreFunSeries.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: MoreFunSeries.v,v 1.4 2004/04/23 10:00:59 lcf Exp $ *)
  20
  21 include "ftc/FunctSeries.ma".
  22
  23 include "ftc/MoreFunctions.ma".
  24
  25 (*#* printing FSeries_Sum %\ensuremath{\sum_{\infty}}% #&sum;'<sub>&infin;</sub># *)
  26
  27 (* UNEXPORTED
  28 Section Definitions
  29 *)
  30
  31 (*#* *More on Sequences and Series
  32
  33 We will now extend our convergence definitions and results for
  34 sequences and series of functions defined in compact intervals to
  35 arbitrary intervals.
  36
  37 %\begin{convention}% Throughout this file, [J] will be an interval,
  38 [f, g] will be sequences of continuous (in [J]) functions and [F,G]
  39 will be continuous (in [J]) functions.
  40 %\end{convention}%
  41
  42 **Sequences
  43
  44 First we will consider the case of sequences.
  45
  46 ***Definitions
  47
  48 Some of the definitions do not make sense in this more general setting
  49 (for instance, because the norm of a function is no longer defined),
  50 but the ones which do we simply adapt in the usual way.
  51 *)
  52
  53 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/J.var".
  54
  55 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/f.var".
  56
  57 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/F.var".
  58
  59 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/contf.var".
  60
  61 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Definitions/contF.var".
  62
  63 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_IR.con".
  64
  65 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_IR.con".
  66
  67 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_IR.con".
  68
  69 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_IR.con".
  70
  71 (*#*
  72 The equivalences between these definitions still hold.
  73 *)
  74
  75 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq'_IR.con".
  76
  77 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_seq2_IR.con".
  78
  79 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_seq_IR.con".
  80
  81 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_real_IR.con".
  82
  83 (* UNEXPORTED
  84 End Definitions
  85 *)
  86
  87 (* UNEXPORTED
  88 Section More_Definitions
  89 *)
  90
  91 (*#*
  92 Limit is defined and works in the same way as before.
  93 *)
  94
  95 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/J.var".
  96
  97 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/f.var".
  98
  99 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/contf.var".
 100
 101 (* begin show *)
 102
 103 alias id "conv" = "cic:/CoRN/ftc/MoreFunSeries/More_Definitions/conv.var".
 104
 105 (* end show *)
 106
 107 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_IR.con".
 108
 109 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_Lim_char.con".
 110
 111 (* UNEXPORTED
 112 End More_Definitions
 113 *)
 114
 115 (* UNEXPORTED
 116 Section Irrelevance_of_Proofs
 117 *)
 118
 119 (*#* ***Basic Properties
 120
 121 Proofs are irrelevant as before---they just have to be present.
 122 *)
 123
 124 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/J.var".
 125
 126 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/f.var".
 127
 128 (* begin show *)
 129
 130 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf.var".
 131
 132 alias id "contf0" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contf0.var".
 133
 134 (* end show *)
 135
 136 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/F.var".
 137
 138 (* begin show *)
 139
 140 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF.var".
 141
 142 alias id "contF0" = "cic:/CoRN/ftc/MoreFunSeries/Irrelevance_of_Proofs/contF0.var".
 143
 144 (* end show *)
 145
 146 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wd_IR.con".
 147
 148 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq2_wd_IR.con".
 149
 150 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq_wd_IR.con".
 151
 152 (* UNEXPORTED
 153 End Irrelevance_of_Proofs
 154 *)
 155
 156 (* UNEXPORTED
 157 Opaque Cauchy_fun_seq_Lim_IR.
 158 *)
 159
 160 (* UNEXPORTED
 161 Section More_Properties
 162 *)
 163
 164 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/J.var".
 165
 166 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/f.var".
 167
 168 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/g.var".
 169
 170 (* begin show *)
 171
 172 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf.var".
 173
 174 alias id "contf0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contf0.var".
 175
 176 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg.var".
 177
 178 alias id "contg0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contg0.var".
 179
 180 (* end show *)
 181
 182 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq'_IR.con".
 183
 184 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/F.var".
 185
 186 alias id "G" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/G.var".
 187
 188 (* begin show *)
 189
 190 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF.var".
 191
 192 alias id "contF0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contF0.var".
 193
 194 alias id "contG" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG.var".
 195
 196 alias id "contG0" = "cic:/CoRN/ftc/MoreFunSeries/More_Properties/contG0.var".
 197
 198 (* end show *)
 199
 200 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl_IR.con".
 201
 202 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr_IR.con".
 203
 204 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdl'_IR.con".
 205
 206 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_seq'_wdr'_IR.con".
 207
 208 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_cont_Lim_IR.con".
 209
 210 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_conv_fun_seq_IR.con".
 211
 212 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_Cauchy_fun_seq_IR.con".
 213
 214 (* UNEXPORTED
 215 End More_Properties
 216 *)
 217
 218 (* UNEXPORTED
 219 Hint Resolve Cauchy_cont_Lim_IR: continuous.
 220 *)
 221
 222 (* UNEXPORTED
 223 Section Algebraic_Properties
 224 *)
 225
 226 (*#* ***Algebraic Properties
 227
 228 Algebraic operations still work well.
 229 *)
 230
 231 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/J.var".
 232
 233 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/f.var".
 234
 235 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/g.var".
 236
 237 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contf.var".
 238
 239 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contg.var".
 240
 241 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FLim_unique_IR.con".
 242
 243 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Cauchy_fun_seq_wd_IR.con".
 244
 245 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_const_IR.con".
 246
 247 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_const_IR.con".
 248
 249 alias id "F" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/F.var".
 250
 251 alias id "G" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/G.var".
 252
 253 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contF.var".
 254
 255 alias id "contG" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/contG.var".
 256
 257 (* begin show *)
 258
 259 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convF.var".
 260
 261 alias id "convG" = "cic:/CoRN/ftc/MoreFunSeries/Algebraic_Properties/convG.var".
 262
 263 (* end show *)
 264
 265 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus'_IR.con".
 266
 267 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus'_IR.con".
 268
 269 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult'_IR.con".
 270
 271 (* UNEXPORTED
 272 End Algebraic_Properties
 273 *)
 274
 275 (* UNEXPORTED
 276 Section More_Algebraic_Properties
 277 *)
 278
 279 (*#*
 280 If we work with the limit function things fit in just as well.
 281 *)
 282
 283 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/J.var".
 284
 285 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/f.var".
 286
 287 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/g.var".
 288
 289 alias id "contf" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contf.var".
 290
 291 alias id "contg" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/contg.var".
 292
 293 (* begin show *)
 294
 295 alias id "Hf" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hf.var".
 296
 297 alias id "Hg" = "cic:/CoRN/ftc/MoreFunSeries/More_Algebraic_Properties/Hg.var".
 298
 299 (* end show *)
 300
 301 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_plus_IR.con".
 302
 303 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_plus.con".
 304
 305 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_inv_IR.con".
 306
 307 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_inv.con".
 308
 309 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_minus_IR.con".
 310
 311 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_minus.con".
 312
 313 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Lim_seq_mult_IR.con".
 314
 315 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_Cauchy_prop_mult.con".
 316
 317 (* UNEXPORTED
 318 End More_Algebraic_Properties
 319 *)
 320
 321 (* UNEXPORTED
 322 Section Other
 323 *)
 324
 325 (*#* ***Miscellaneous
 326
 327 Finally, we define a mapping between sequences of real numbers and sequences of (constant) functions and prove that convergence is preserved.
 328 *)
 329
 330 inline procedural "cic:/CoRN/ftc/MoreFunSeries/seq_to_funseq.con".
 331
 332 inline procedural "cic:/CoRN/ftc/MoreFunSeries/funseq_conv.con".
 333
 334 (*#*
 335 Another interesting fact: if a sequence of constant functions converges then it must converge to a constant function.
 336 *)
 337
 338 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_const_Lim.con".
 339
 340 (* UNEXPORTED
 341 End Other
 342 *)
 343
 344 (* UNEXPORTED
 345 Section Series_Definitions
 346 *)
 347
 348 (*#* **Series
 349
 350 We now consider series of functions defined in arbitrary intervals.
 351
 352 Convergence is defined as expected---through convergence in every compact interval.
 353 *)
 354
 355 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/J.var".
 356
 357 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/f.var".
 358
 359 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_IR.con".
 360
 361 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_conv_imp_conv_IR.con".
 362
 363 (* begin show *)
 364
 365 alias id "H" = "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/H.var".
 366
 367 (* end show *)
 368
 369 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_inc_IR.con".
 370
 371 (*#* Assume [h(x)] is the pointwise series of [f(x)] *)
 372
 373 (* begin hide *)
 374
 375 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Series_Definitions/h.con" "Series_Definitions__".
 376
 377 (* end hide *)
 378
 379 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_strext_IR.con".
 380
 381 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum.con".
 382
 383 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_char.con".
 384
 385 (* UNEXPORTED
 386 End Series_Definitions
 387 *)
 388
 389 (* UNEXPORTED
 390 Implicit Arguments FSeries_Sum [J f].
 391 *)
 392
 393 (* UNEXPORTED
 394 Section More_Series_Definitions
 395 *)
 396
 397 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/J.var".
 398
 399 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/More_Series_Definitions/f.var".
 400
 401 (*#*
 402 Absolute convergence still exists.
 403 *)
 404
 405 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_abs_convergent_IR.con".
 406
 407 (* UNEXPORTED
 408 End More_Series_Definitions
 409 *)
 410
 411 (* UNEXPORTED
 412 Section Convergence_Results
 413 *)
 414
 415 (*#*
 416 As before, any series converges to its sum.
 417 *)
 418
 419 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/J.var".
 420
 421 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Results/f.var".
 422
 423 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_conv.con".
 424
 425 inline procedural "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_inc.con".
 426
 427 inline procedural "cic:/CoRN/ftc/MoreFunSeries/convergent_imp_Continuous.con".
 428
 429 inline procedural "cic:/CoRN/ftc/MoreFunSeries/Continuous_FSeries_Sum.con".
 430
 431 (* UNEXPORTED
 432 End Convergence_Results
 433 *)
 434
 435 (* UNEXPORTED
 436 Hint Resolve convergent_imp_inc: included.
 437 *)
 438
 439 (* UNEXPORTED
 440 Hint Resolve convergent_imp_Continuous Continuous_FSeries_Sum: continuous.
 441 *)
 442
 443 (* UNEXPORTED
 444 Section Operations
 445 *)
 446
 447 (*#* **Algebraic Operations
 448
 449 Convergence is well defined and preserved by operations.
 450 *)
 451
 452 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Operations/J.var".
 453
 454 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_fun_const_series_IR.con".
 455
 456 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_const_series_Sum_IR.con".
 457
 458 inline procedural "cic:/CoRN/ftc/MoreFunSeries/conv_zero_fun_series_IR.con".
 459
 460 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_zero_IR.con".
 461
 462 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Operations/f.var".
 463
 464 alias id "g" = "cic:/CoRN/ftc/MoreFunSeries/Operations/g.var".
 465
 466 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_series_convergent_wd_IR.con".
 467
 468 (* begin show *)
 469
 470 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Operations/convF.var".
 471
 472 alias id "convG" = "cic:/CoRN/ftc/MoreFunSeries/Operations/convG.var".
 473
 474 (* end show *)
 475
 476 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_wd'.con".
 477
 478 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus_conv.con".
 479
 480 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_plus.con".
 481
 482 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv_conv.con".
 483
 484 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_inv.con".
 485
 486 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus_conv.con".
 487
 488 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_minus.con".
 489
 490 (*#*
 491 %\begin{convention}% Let [c:IR] and [H:PartIR] be continuous in [J].
 492 %\end{convention}%
 493 *)
 494
 495 alias id "c" = "cic:/CoRN/ftc/MoreFunSeries/Operations/c.var".
 496
 497 alias id "H" = "cic:/CoRN/ftc/MoreFunSeries/Operations/H.var".
 498
 499 alias id "contH" = "cic:/CoRN/ftc/MoreFunSeries/Operations/contH.var".
 500
 501 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal_conv.con".
 502
 503 inline procedural "cic:/CoRN/ftc/MoreFunSeries/FSeries_Sum_scal.con".
 504
 505 (* UNEXPORTED
 506 End Operations
 507 *)
 508
 509 (* UNEXPORTED
 510 Section Convergence_Criteria
 511 *)
 512
 513 (*#* ***Convergence Criteria
 514
 515 The most important tests for convergence of series still apply: the
 516 comparison test (in both versions) and the ratio test.
 517 *)
 518
 519 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/J.var".
 520
 521 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/f.var".
 522
 523 alias id "contF" = "cic:/CoRN/ftc/MoreFunSeries/Convergence_Criteria/contF.var".
 524
 525 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_str_comparison_IR.con".
 526
 527 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_comparison_IR.con".
 528
 529 inline procedural "cic:/CoRN/ftc/MoreFunSeries/abs_imp_conv_IR.con".
 530
 531 inline procedural "cic:/CoRN/ftc/MoreFunSeries/fun_ratio_test_conv_IR.con".
 532
 533 (* UNEXPORTED
 534 End Convergence_Criteria
 535 *)
 536
 537 (* UNEXPORTED
 538 Section Insert_Series
 539 *)
 540
 541 (*#* ***Translation
 542
 543 When working in particular with power series and Taylor series, it is
 544 sometimes useful to ``shift'' all the terms in the series one position
 545 forward, that is, replacing each $f_{i+1}$#f<sub>i+1</sub># with
 546 $f_i$#f<sub>i</sub># and inserting the null function in the first
 547 position.  This does not affect convergence or the sum of the series.
 548 *)
 549
 550 alias id "J" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/J.var".
 551
 552 alias id "f" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/f.var".
 553
 554 alias id "convF" = "cic:/CoRN/ftc/MoreFunSeries/Insert_Series/convF.var".
 555
 556 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series.con".
 557
 558 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_cont.con".
 559
 560 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum_char.con".
 561
 562 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_conv.con".
 563
 564 inline procedural "cic:/CoRN/ftc/MoreFunSeries/insert_series_sum.con".
 565
 566 (* UNEXPORTED
 567 End Insert_Series
 568 *)
 569