cfcont_1.miz



    begin

    reserve n,n1,m,m1,k for Nat;

    reserve x,X,X1 for set;

    reserve g,g1,g2,t,x0,x1,x2 for Complex;

    reserve s1,s2,q1,seq,seq1,seq2,seq3 for Complex_Sequence;

    reserve Y for Subset of COMPLEX ;

    reserve f,f1,f2,h,h1,h2 for PartFunc of COMPLEX , COMPLEX ;

    reserve p,r,s for Real;

    reserve Ns,Nseq for increasing sequence of NAT ;

    definition

      let f, x0;

      :: CFCONT_1:def1

      pred f is_continuous_in x0 means x0 in ( dom f) & for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

    end

    theorem :: CFCONT_1:1

    

     Th1: seq1 = (seq2 - seq3) iff for n holds (seq1 . n) = ((seq2 . n) - (seq3 . n))

    proof

      thus seq1 = (seq2 - seq3) implies for n holds (seq1 . n) = ((seq2 . n) - (seq3 . n))

      proof

        assume

         A1: seq1 = (seq2 - seq3);

        now

          let n;

          

           A2: n in NAT by ORDINAL1:def 12;

          (seq1 . n) = ((seq2 . n) + (( - seq3) . n)) by A1, VALUED_1: 1, A2;

          then (seq1 . n) = ((seq2 . n) + ( - (seq3 . n))) by VALUED_1: 8;

          hence (seq1 . n) = ((seq2 . n) - (seq3 . n));

        end;

        hence thesis;

      end;

      assume

       A3: for n holds (seq1 . n) = ((seq2 . n) - (seq3 . n));

      now

        let n be Element of NAT ;

        

        thus (seq1 . n) = ((seq2 . n) - (seq3 . n)) by A3

        .= ((seq2 . n) + ( - (seq3 . n)))

        .= ((seq2 . n) + (( - seq3) . n)) by VALUED_1: 8

        .= ((seq2 + ( - seq3)) . n) by VALUED_1: 1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:2

    

     Th2: ((seq1 + seq2) * Ns) = ((seq1 * Ns) + (seq2 * Ns)) & ((seq1 - seq2) * Ns) = ((seq1 * Ns) - (seq2 * Ns)) & ((seq1 (#) seq2) * Ns) = ((seq1 * Ns) (#) (seq2 * Ns))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq1 + seq2) * Ns) . n) = ((seq1 + seq2) . (Ns . n)) by FUNCT_2: 15

        .= ((seq1 . (Ns . n)) + (seq2 . (Ns . n))) by VALUED_1: 1

        .= (((seq1 * Ns) . n) + (seq2 . (Ns . n))) by FUNCT_2: 15

        .= (((seq1 * Ns) . n) + ((seq2 * Ns) . n)) by FUNCT_2: 15

        .= (((seq1 * Ns) + (seq2 * Ns)) . n) by VALUED_1: 1;

      end;

      hence ((seq1 + seq2) * Ns) = ((seq1 * Ns) + (seq2 * Ns)) by FUNCT_2: 63;

      now

        let n be Element of NAT ;

        

        thus (((seq1 - seq2) * Ns) . n) = ((seq1 - seq2) . (Ns . n)) by FUNCT_2: 15

        .= ((seq1 . (Ns . n)) - (seq2 . (Ns . n))) by Th1

        .= (((seq1 * Ns) . n) - (seq2 . (Ns . n))) by FUNCT_2: 15

        .= (((seq1 * Ns) . n) - ((seq2 * Ns) . n)) by FUNCT_2: 15

        .= (((seq1 * Ns) - (seq2 * Ns)) . n) by Th1;

      end;

      hence ((seq1 - seq2) * Ns) = ((seq1 * Ns) - (seq2 * Ns)) by FUNCT_2: 63;

      now

        let n be Element of NAT ;

        

        thus (((seq1 (#) seq2) * Ns) . n) = ((seq1 (#) seq2) . (Ns . n)) by FUNCT_2: 15

        .= ((seq1 . (Ns . n)) * (seq2 . (Ns . n))) by VALUED_1: 5

        .= (((seq1 * Ns) . n) * (seq2 . (Ns . n))) by FUNCT_2: 15

        .= (((seq1 * Ns) . n) * ((seq2 * Ns) . n)) by FUNCT_2: 15

        .= (((seq1 * Ns) (#) (seq2 * Ns)) . n) by VALUED_1: 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:3

    

     Th3: ((g (#) seq) * Ns) = (g (#) (seq * Ns))

    proof

      now

        let n be Element of NAT ;

        

        thus (((g (#) seq) * Ns) . n) = ((g (#) seq) . (Ns . n)) by FUNCT_2: 15

        .= (g * (seq . (Ns . n))) by VALUED_1: 6

        .= (g * ((seq * Ns) . n)) by FUNCT_2: 15

        .= ((g (#) (seq * Ns)) . n) by VALUED_1: 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:4

    (( - seq) * Ns) = ( - (seq * Ns)) & ( |.seq.| * Ns) = |.(seq * Ns).|

    proof

      

      thus (( - seq) * Ns) = ((( - 1r ) (#) seq) * Ns) by COMSEQ_1: 11

      .= (( - 1r ) (#) (seq * Ns)) by Th3

      .= ( - (seq * Ns)) by COMSEQ_1: 11;

      now

        let n be Element of NAT ;

        

        thus (( |.seq.| * Ns) . n) = ( |.seq.| . (Ns . n)) by FUNCT_2: 15

        .= |.(seq . (Ns . n)).| by VALUED_1: 18

        .= |.((seq * Ns) . n).| by FUNCT_2: 15

        .= ( |.(seq * Ns).| . n) by VALUED_1: 18;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:5

    

     Th5: ((seq * Ns) " ) = ((seq " ) * Ns)

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq * Ns) " ) . n) = (((seq * Ns) . n) " ) by VALUED_1: 10

        .= ((seq . (Ns . n)) " ) by FUNCT_2: 15

        .= ((seq " ) . (Ns . n)) by VALUED_1: 10

        .= (((seq " ) * Ns) . n) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:6

    ((seq1 /" seq) * Ns) = ((seq1 * Ns) /" (seq * Ns))

    proof

      

      thus ((seq1 /" seq) * Ns) = ((seq1 * Ns) (#) ((seq " ) * Ns)) by Th2

      .= ((seq1 * Ns) /" (seq * Ns)) by Th5;

    end;

    theorem :: CFCONT_1:7

    

     Th7: ( rng seq) c= (( dom h1) /\ ( dom h2)) implies ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) & ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq)) & ((h1 (#) h2) /* seq) = ((h1 /* seq) (#) (h2 /* seq))

    proof

      

       A1: (( dom h1) /\ ( dom h2)) c= ( dom h1) by XBOOLE_1: 17;

      

       A2: (( dom h1) /\ ( dom h2)) c= ( dom h2) by XBOOLE_1: 17;

      assume

       A3: ( rng seq) c= (( dom h1) /\ ( dom h2));

      then

       A4: ( rng seq) c= ( dom (h1 + h2)) by VALUED_1:def 1;

      now

        let n be Element of NAT ;

        

         A5: (seq . n) in ( rng seq) by VALUED_0: 28;

        

        thus (((h1 + h2) /* seq) . n) = ((h1 + h2) /. (seq . n)) by A4, FUNCT_2: 109

        .= ((h1 /. (seq . n)) + (h2 /. (seq . n))) by A4, A5, CFUNCT_1: 1

        .= (((h1 /* seq) . n) + (h2 /. (seq . n))) by A3, A1, FUNCT_2: 109, XBOOLE_1: 1

        .= (((h1 /* seq) . n) + ((h2 /* seq) . n)) by A3, A2, FUNCT_2: 109, XBOOLE_1: 1

        .= (((h1 /* seq) + (h2 /* seq)) . n) by VALUED_1: 1;

      end;

      hence ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) by FUNCT_2: 63;

      

       A6: ( rng seq) c= ( dom (h1 - h2)) by A3, CFUNCT_1: 2;

      now

        let n;

        

         A7: n in NAT by ORDINAL1:def 12;

        

         A8: (seq . n) in ( rng seq) by VALUED_0: 28;

        

        thus (((h1 - h2) /* seq) . n) = ((h1 - h2) /. (seq . n)) by A6, FUNCT_2: 109, A7

        .= ((h1 /. (seq . n)) - (h2 /. (seq . n))) by A6, A8, CFUNCT_1: 2

        .= (((h1 /* seq) . n) - (h2 /. (seq . n))) by A3, A1, FUNCT_2: 109, XBOOLE_1: 1, A7

        .= (((h1 /* seq) . n) - ((h2 /* seq) . n)) by A3, A2, FUNCT_2: 109, XBOOLE_1: 1, A7;

      end;

      hence ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq)) by Th1;

      

       A9: ( rng seq) c= ( dom (h1 (#) h2)) by A3, VALUED_1:def 4;

      now

        let n be Element of NAT ;

        

         A10: (seq . n) in ( rng seq) by VALUED_0: 28;

        

        thus (((h1 (#) h2) /* seq) . n) = ((h1 (#) h2) /. (seq . n)) by A9, FUNCT_2: 109

        .= ((h1 /. (seq . n)) * (h2 /. (seq . n))) by A9, A10, CFUNCT_1: 3

        .= (((h1 /* seq) . n) * (h2 /. (seq . n))) by A3, A1, FUNCT_2: 109, XBOOLE_1: 1

        .= (((h1 /* seq) . n) * ((h2 /* seq) . n)) by A3, A2, FUNCT_2: 109, XBOOLE_1: 1

        .= (((h1 /* seq) (#) (h2 /* seq)) . n) by VALUED_1: 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:8

    

     Th8: ( rng seq) c= ( dom h) implies ((g (#) h) /* seq) = (g (#) (h /* seq))

    proof

      assume

       A1: ( rng seq) c= ( dom h);

      then

       A2: ( rng seq) c= ( dom (g (#) h)) by VALUED_1:def 5;

      now

        let n be Element of NAT ;

        

         A3: (seq . n) in ( rng seq) by VALUED_0: 28;

        

        thus (((g (#) h) /* seq) . n) = ((g (#) h) /. (seq . n)) by A2, FUNCT_2: 109

        .= (g * (h /. (seq . n))) by A2, A3, CFUNCT_1: 4

        .= (g * ((h /* seq) . n)) by A1, FUNCT_2: 109

        .= ((g (#) (h /* seq)) . n) by VALUED_1: 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:9

    ( rng seq) c= ( dom h) implies ( - (h /* seq)) = (( - h) /* seq) by Th8;

    theorem :: CFCONT_1:10

    

     Th10: ( rng seq) c= ( dom (h ^ )) implies (h /* seq) is non-zero

    proof

      assume

       A1: ( rng seq) c= ( dom (h ^ ));

      then

       A2: (( dom h) \ (h " { 0c })) c= ( dom h) & ( rng seq) c= (( dom h) \ (h " { 0c })) by CFUNCT_1:def 2, XBOOLE_1: 36;

      now

        given n be Element of NAT such that

         A3: ((h /* seq) . n) = 0c ;

        (seq . n) in ( rng seq) by VALUED_0: 28;

        then (seq . n) in ( dom (h ^ )) by A1;

        then (seq . n) in (( dom h) \ (h " { 0c })) by CFUNCT_1:def 2;

        then (seq . n) in ( dom h) & not (seq . n) in (h " { 0c }) by XBOOLE_0:def 5;

        then

         A4: not (h /. (seq . n)) in { 0c } by PARTFUN2: 26;

        (h /. (seq . n)) = 0c by A2, A3, FUNCT_2: 109, XBOOLE_1: 1;

        hence contradiction by A4, TARSKI:def 1;

      end;

      hence thesis by COMSEQ_1: 4;

    end;

    theorem :: CFCONT_1:11

    

     Th11: ( rng seq) c= ( dom (h ^ )) implies ((h ^ ) /* seq) = ((h /* seq) " )

    proof

      assume

       A1: ( rng seq) c= ( dom (h ^ ));

      then

       A2: (( dom h) \ (h " { 0c })) c= ( dom h) & ( rng seq) c= (( dom h) \ (h " { 0c })) by CFUNCT_1:def 2, XBOOLE_1: 36;

      now

        let n be Element of NAT ;

        

         A3: (seq . n) in ( rng seq) by VALUED_0: 28;

        

        thus (((h ^ ) /* seq) . n) = ((h ^ ) /. (seq . n)) by A1, FUNCT_2: 109

        .= ((h /. (seq . n)) " ) by A1, A3, CFUNCT_1:def 2

        .= (((h /* seq) . n) " ) by A2, FUNCT_2: 109, XBOOLE_1: 1

        .= (((h /* seq) " ) . n) by VALUED_1: 10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:12

    ( rng seq) c= ( dom h) implies ( Re ((h /* seq) * Ns)) = ( Re (h /* (seq * Ns)))

    proof

      assume

       A1: ( rng seq) c= ( dom h);

      now

        let n be Element of NAT ;

        (seq * Ns) is subsequence of seq by VALUED_0:def 17;

        then

         A2: ( rng (seq * Ns)) c= ( rng seq) by VALUED_0: 21;

        

        thus (( Re ((h /* seq) * Ns)) . n) = ( Re (((h /* seq) * Ns) . n)) by COMSEQ_3:def 5

        .= ( Re ((h /* seq) . (Ns . n))) by FUNCT_2: 15

        .= ( Re (h /. (seq . (Ns . n)))) by A1, FUNCT_2: 109

        .= ( Re (h /. ((seq * Ns) . n))) by FUNCT_2: 15

        .= ( Re ((h /* (seq * Ns)) . n)) by A1, A2, FUNCT_2: 109, XBOOLE_1: 1

        .= (( Re (h /* (seq * Ns))) . n) by COMSEQ_3:def 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:13

    ( rng seq) c= ( dom h) implies ( Im ((h /* seq) * Ns)) = ( Im (h /* (seq * Ns)))

    proof

      assume

       A1: ( rng seq) c= ( dom h);

      now

        let n be Element of NAT ;

        (seq * Ns) is subsequence of seq by VALUED_0:def 17;

        then

         A2: ( rng (seq * Ns)) c= ( rng seq) by VALUED_0: 21;

        

        thus (( Im ((h /* seq) * Ns)) . n) = ( Im (((h /* seq) * Ns) . n)) by COMSEQ_3:def 6

        .= ( Im ((h /* seq) . (Ns . n))) by FUNCT_2: 15

        .= ( Im (h /. (seq . (Ns . n)))) by A1, FUNCT_2: 109

        .= ( Im (h /. ((seq * Ns) . n))) by FUNCT_2: 15

        .= ( Im ((h /* (seq * Ns)) . n)) by A1, A2, FUNCT_2: 109, XBOOLE_1: 1

        .= (( Im (h /* (seq * Ns))) . n) by COMSEQ_3:def 6;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:14

    h1 is total & h2 is total implies ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) & ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq)) & ((h1 (#) h2) /* seq) = ((h1 /* seq) (#) (h2 /* seq))

    proof

      assume h1 is total & h2 is total;

      then ( dom (h1 + h2)) = COMPLEX by PARTFUN1:def 2;

      then (( dom h1) /\ ( dom h2)) = COMPLEX by VALUED_1:def 1;

      then

       A1: ( rng seq) c= (( dom h1) /\ ( dom h2));

      hence ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) by Th7;

      thus ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq)) by A1, Th7;

      thus thesis by A1, Th7;

    end;

    theorem :: CFCONT_1:15

    h is total implies ((g (#) h) /* seq) = (g (#) (h /* seq))

    proof

      assume h is total;

      then ( dom h) = COMPLEX by PARTFUN1:def 2;

      then ( rng seq) c= ( dom h);

      hence thesis by Th8;

    end;

    theorem :: CFCONT_1:16

    ( rng seq) c= ( dom (h | X)) & (h " { 0 }) = {} implies (((h ^ ) | X) /* seq) = (((h | X) /* seq) " )

    proof

      assume that

       A1: ( rng seq) c= ( dom (h | X)) and

       A2: (h " { 0 }) = {} ;

      now

        let x be object;

        assume x in ( rng seq);

        then x in ( dom (h | X)) by A1;

        then

         A3: x in (( dom h) /\ X) by RELAT_1: 61;

        then x in (( dom h) \ (h " { 0c })) by A2, XBOOLE_0:def 4;

        then

         A4: x in ( dom (h ^ )) by CFUNCT_1:def 2;

        x in X by A3, XBOOLE_0:def 4;

        then x in (( dom (h ^ )) /\ X) by A4, XBOOLE_0:def 4;

        hence x in ( dom ((h ^ ) | X)) by RELAT_1: 61;

      end;

      then

       A5: ( rng seq) c= ( dom ((h ^ ) | X));

      now

        let n be Element of NAT ;

        

         A6: (seq . n) in ( rng seq) by VALUED_0: 28;

        then (seq . n) in ( dom (h | X)) by A1;

        then

         A7: (seq . n) in (( dom h) /\ X) by RELAT_1: 61;

        then (seq . n) in (( dom h) \ (h " { 0c })) by A2, XBOOLE_0:def 4;

        then

         A8: (seq . n) in ( dom (h ^ )) by CFUNCT_1:def 2;

        (seq . n) in X by A7, XBOOLE_0:def 4;

        then (seq . n) in (( dom (h ^ )) /\ X) by A8, XBOOLE_0:def 4;

        then

         A9: (seq . n) in ( dom ((h ^ ) | X)) by RELAT_1: 61;

        

        thus ((((h ^ ) | X) /* seq) . n) = (((h ^ ) | X) /. (seq . n)) by A5, FUNCT_2: 109

        .= ((h ^ ) /. (seq . n)) by A9, PARTFUN2: 15

        .= ((h /. (seq . n)) " ) by A8, CFUNCT_1:def 2

        .= (((h | X) /. (seq . n)) " ) by A1, A6, PARTFUN2: 15

        .= ((((h | X) /* seq) . n) " ) by A1, FUNCT_2: 109

        .= ((((h | X) /* seq) " ) . n) by VALUED_1: 10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: CFCONT_1:17

    

     Th17: seq1 is subsequence of seq & seq is convergent implies seq1 is convergent

    proof

      assume that

       A1: seq1 is subsequence of seq and

       A2: seq is convergent;

      consider g be Complex such that

       A3: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g).| < p by A2;

      take t = g;

      let p;

      assume 0 < p;

      then

      consider n1 such that

       A4: for m st n1 <= m holds |.((seq . m) - g).| < p by A3;

      take n = n1;

      let m such that

       A5: n <= m;

      consider Nseq such that

       A6: seq1 = (seq * Nseq) by A1, VALUED_0:def 17;

      m <= (Nseq . m) by SEQM_3: 14;

      then

       A7: n <= (Nseq . m) by A5, XXREAL_0: 2;

      m in NAT by ORDINAL1:def 12;

      then (seq1 . m) = (seq . (Nseq . m)) by A6, FUNCT_2: 15;

      hence |.((seq1 . m) - t).| < p by A4, A7;

    end;

    theorem :: CFCONT_1:18

    

     Th18: seq1 is subsequence of seq & seq is convergent implies ( lim seq1) = ( lim seq)

    proof

      assume that

       A1: seq1 is subsequence of seq and

       A2: seq is convergent;

      consider Nseq such that

       A3: seq1 = (seq * Nseq) by A1, VALUED_0:def 17;

       A4:

      now

        let p;

        assume 0 < p;

        then

        consider n1 such that

         A5: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < p by A2, COMSEQ_2:def 6;

        take n = n1;

        let m such that

         A6: n <= m;

        m <= (Nseq . m) by SEQM_3: 14;

        then

         A7: n <= (Nseq . m) by A6, XXREAL_0: 2;

        

         A8: m in NAT by ORDINAL1:def 12;

        (seq1 . m) = (seq . (Nseq . m)) by A3, FUNCT_2: 15, A8;

        hence |.((seq1 . m) - ( lim seq)).| < p by A5, A7;

      end;

      seq1 is convergent by A1, A2, Th17;

      hence thesis by A4, COMSEQ_2:def 6;

    end;

    theorem :: CFCONT_1:19

    

     Th19: seq is convergent & (ex k st for n st k <= n holds (seq1 . n) = (seq . n)) implies seq1 is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: ex k st for n st k <= n holds (seq1 . n) = (seq . n);

      consider g1 be Complex such that

       A3: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p by A1;

      consider k such that

       A4: for n st k <= n holds (seq1 . n) = (seq . n) by A2;

      take g = g1;

      let p;

      assume 0 < p;

      then

      consider n1 such that

       A5: for m st n1 <= m holds |.((seq . m) - g1).| < p by A3;

       A6:

      now

        assume

         A7: n1 <= k;

        take n = k;

        let m;

        assume

         A8: n <= m;

        then n1 <= m by A7, XXREAL_0: 2;

        then |.((seq . m) - g1).| < p by A5;

        hence |.((seq1 . m) - g).| < p by A4, A8;

      end;

      now

        assume

         A9: k <= n1;

        take n = n1;

        let m;

        assume

         A10: n <= m;

        then (seq1 . m) = (seq . m) by A4, A9, XXREAL_0: 2;

        hence |.((seq1 . m) - g).| < p by A5, A10;

      end;

      hence ex n st for m st n <= m holds |.((seq1 . m) - g).| < p by A6;

    end;

    theorem :: CFCONT_1:20

    seq is convergent & (ex k st for n st k <= n holds (seq1 . n) = (seq . n)) implies ( lim seq) = ( lim seq1)

    proof

      assume that

       A1: seq is convergent and

       A2: ex k st for n st k <= n holds (seq1 . n) = (seq . n);

      consider k such that

       A3: for n st k <= n holds (seq1 . n) = (seq . n) by A2;

       A4:

      now

        let p;

        assume 0 < p;

        then

        consider n1 such that

         A5: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < p by A1, COMSEQ_2:def 6;

         A6:

        now

          assume

           A7: n1 <= k;

          take n = k;

          let m;

          assume

           A8: n <= m;

          then n1 <= m by A7, XXREAL_0: 2;

          then |.((seq . m) - ( lim seq)).| < p by A5;

          hence |.((seq1 . m) - ( lim seq)).| < p by A3, A8;

        end;

        now

          assume

           A9: k <= n1;

          take n = n1;

          let m;

          assume

           A10: n <= m;

          then (seq1 . m) = (seq . m) by A3, A9, XXREAL_0: 2;

          hence |.((seq1 . m) - ( lim seq)).| < p by A5, A10;

        end;

        hence ex n st for m st n <= m holds |.((seq1 . m) - ( lim seq)).| < p by A6;

      end;

      seq1 is convergent by A1, A2, Th19;

      hence thesis by A4, COMSEQ_2:def 6;

    end;

    theorem :: CFCONT_1:21

    seq is convergent implies (seq ^\ k) is convergent & ( lim (seq ^\ k)) = ( lim seq) by Th17, Th18;

    theorem :: CFCONT_1:22

    

     Th22: seq is convergent & (ex k st seq = (seq1 ^\ k)) implies seq1 is convergent

    proof

      assume that

       A1: seq is convergent and

       A2: ex k st seq = (seq1 ^\ k);

      consider k such that

       A3: seq = (seq1 ^\ k) by A2;

      consider g1 be Complex such that

       A4: for p st 0 < p holds ex n st for m st n <= m holds |.((seq . m) - g1).| < p by A1;

      take g = g1;

      let p;

      assume 0 < p;

      then

      consider n1 such that

       A5: for m st n1 <= m holds |.((seq . m) - g1).| < p by A4;

      take n = (n1 + k);

      let m;

      assume

       A6: n <= m;

      then

      consider l be Nat such that

       A7: m = ((n1 + k) + l) by NAT_1: 10;

      reconsider l as Element of NAT by ORDINAL1:def 12;

      (m - k) = (((n1 + l) + k) + ( - k)) by A7;

      then

      consider m1 such that

       A8: m1 = (m - k);

      now

        assume not n1 <= m1;

        then (m1 + k) < (n1 + k) by XREAL_1: 6;

        hence contradiction by A6, A8;

      end;

      then

       A9: |.((seq . m1) - g1).| < p by A5;

      (m1 + k) = m by A8;

      hence |.((seq1 . m) - g).| < p by A3, A9, NAT_1:def 3;

    end;

    theorem :: CFCONT_1:23

    seq is convergent & (ex k st seq = (seq1 ^\ k)) implies ( lim seq1) = ( lim seq)

    proof

      assume that

       A1: seq is convergent and

       A2: ex k st seq = (seq1 ^\ k);

      consider k such that

       A3: seq = (seq1 ^\ k) by A2;

       A4:

      now

        let p;

        assume 0 < p;

        then

        consider n1 such that

         A5: for m st n1 <= m holds |.((seq . m) - ( lim seq)).| < p by A1, COMSEQ_2:def 6;

        take n = (n1 + k);

        let m;

        assume

         A6: n <= m;

        then

        consider l be Nat such that

         A7: m = ((n1 + k) + l) by NAT_1: 10;

        reconsider l as Element of NAT by ORDINAL1:def 12;

        (m - k) = (((n1 + l) + k) + ( - k)) by A7;

        then

        consider m1 such that

         A8: m1 = (m - k);

        now

          assume not n1 <= m1;

          then (m1 + k) < (n1 + k) by XREAL_1: 6;

          hence contradiction by A6, A8;

        end;

        then

         A9: |.((seq . m1) - ( lim seq)).| < p by A5;

        (m1 + k) = m by A8;

        hence |.((seq1 . m) - ( lim seq)).| < p by A3, A9, NAT_1:def 3;

      end;

      seq1 is convergent by A1, A2, Th22;

      hence thesis by A4, COMSEQ_2:def 6;

    end;

    theorem :: CFCONT_1:24

    

     Th24: seq is convergent & ( lim seq) <> 0 implies ex k st (seq ^\ k) is non-zero

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) <> 0 ;

      consider n1 such that

       A3: for m st n1 <= m holds ( |.( lim seq).| / 2) < |.(seq . m).| by A1, A2, COMSEQ_2: 33;

      take k = n1;

      now

        let n be Element of NAT ;

        ( 0 + k) <= (n + k) by XREAL_1: 7;

        then ( |.( lim seq).| / 2) < |.(seq . (n + k)).| by A3;

        then

         A4: ( |.( lim seq).| / 2) < |.((seq ^\ k) . n).| by NAT_1:def 3;

         0 < |.( lim seq).| by A2, COMPLEX1: 47;

        then ( 0 / 2) < ( |.( lim seq).| / 2) by XREAL_1: 74;

        then 0 < |.((seq ^\ k) . n).| by A4;

        hence ((seq ^\ k) . n) <> 0c by COMPLEX1: 47;

      end;

      hence thesis by COMSEQ_1: 4;

    end;

    theorem :: CFCONT_1:25

    seq is convergent & ( lim seq) <> 0 implies ex seq1 st seq1 is subsequence of seq & seq1 is non-zero

    proof

      assume seq is convergent & ( lim seq) <> 0 ;

      then

      consider k such that

       A1: (seq ^\ k) is non-zero by Th24;

      take (seq ^\ k);

      thus thesis by A1;

    end;

    theorem :: CFCONT_1:26

    

     Th26: seq is constant implies seq is convergent

    proof

      assume seq is constant;

      then

      consider t be Element of COMPLEX such that

       A1: for n be Nat holds (seq . n) = t by VALUED_0:def 18;

      take g = t;

      let p such that

       A2: 0 < p;

      take n = 0 ;

      let m such that n <= m;

       |.((seq . m) - g).| = |.(t - g).| by A1

      .= 0 by COMPLEX1: 44;

      hence |.((seq . m) - g).| < p by A2;

    end;

    theorem :: CFCONT_1:27

    

     Th27: (seq is constant & g in ( rng seq) or seq is constant & ex n st (seq . n) = g) implies ( lim seq) = g

    proof

       A1:

      now

        assume that

         A2: seq is constant and

         A3: g in ( rng seq);

        consider g1 be Element of COMPLEX such that

         A4: ( rng seq) = {g1} by A2, FUNCT_2: 111;

        consider g2 be Element of COMPLEX such that

         A5: for n be Nat holds (seq . n) = g2 by A2, VALUED_0:def 18;

        

         A6: g = g1 by A3, A4, TARSKI:def 1;

         A7:

        now

          let p such that

           A8: 0 < p;

          reconsider n = 0 as Nat;

          take n;

          let m such that n <= m;

          m in NAT by ORDINAL1:def 12;

          then m in ( dom seq) by COMSEQ_1: 2;

          then (seq . m) in ( rng seq) by FUNCT_1:def 3;

          then g2 in ( rng seq) by A5;

          then g2 = g by A4, A6, TARSKI:def 1;

          then (seq . m) = g by A5;

          hence |.((seq . m) - g).| < p by A8, COMPLEX1: 44;

        end;

        seq is convergent by A2, Th26;

        hence thesis by A7, COMSEQ_2:def 6;

      end;

       A9:

      now

        assume that seq is constant and

         A10: ex n st (seq . n) = g;

        consider n such that

         A11: (seq . n) = g by A10;

        n in NAT by ORDINAL1:def 12;

        then n in ( dom seq) by COMSEQ_1: 2;

        hence thesis by A1, A11, FUNCT_1:def 3;

      end;

      assume seq is constant & g in ( rng seq) or seq is constant & ex n be Nat st (seq . n) = g;

      hence thesis by A1, A9;

    end;

    theorem :: CFCONT_1:28

    seq is constant implies for n holds ( lim seq) = (seq . n) by Th27;

    theorem :: CFCONT_1:29

    seq is convergent & ( lim seq) <> 0 implies for seq1 st seq1 is subsequence of seq & seq1 is non-zero holds ( lim (seq1 " )) = (( lim seq) " )

    proof

      assume that

       A1: seq is convergent and

       A2: ( lim seq) <> 0 ;

      let seq1 such that

       A3: seq1 is subsequence of seq and

       A4: seq1 is non-zero;

      ( lim seq1) = ( lim seq) by A1, A3, Th18;

      hence thesis by A1, A2, A3, A4, Th17, COMSEQ_2: 35;

    end;

    theorem :: CFCONT_1:30

    seq is constant & seq1 is convergent implies ( lim (seq + seq1)) = ((seq . 0 ) + ( lim seq1)) & ( lim (seq - seq1)) = ((seq . 0 ) - ( lim seq1)) & ( lim (seq1 - seq)) = (( lim seq1) - (seq . 0 )) & ( lim (seq (#) seq1)) = ((seq . 0 ) * ( lim seq1))

    proof

      assume that

       A1: seq is constant and

       A2: seq1 is convergent;

      

       A3: seq is convergent by A1, Th26;

      

      hence ( lim (seq + seq1)) = (( lim seq) + ( lim seq1)) by A2, COMSEQ_2: 14

      .= ((seq . 0 ) + ( lim seq1)) by A1, Th27;

      

      thus ( lim (seq - seq1)) = (( lim seq) - ( lim seq1)) by A2, A3, COMSEQ_2: 26

      .= ((seq . 0 ) - ( lim seq1)) by A1, Th27;

      

      thus ( lim (seq1 - seq)) = (( lim seq1) - ( lim seq)) by A2, A3, COMSEQ_2: 26

      .= (( lim seq1) - (seq . 0 )) by A1, Th27;

      

      thus ( lim (seq (#) seq1)) = (( lim seq) * ( lim seq1)) by A2, A3, COMSEQ_2: 30

      .= ((seq . 0 ) * ( lim seq1)) by A1, Th27;

    end;

    scheme :: CFCONT_1:sch1

    CompSeqChoice { P[ object, object] } :

ex s1 st for n holds P[n, (s1 . n)]

      provided

       A1: for n holds ex g st P[n, g];

      

       A2: for t be Element of NAT holds ex ff be Element of COMPLEX st P[t, ff]

      proof

        let t be Element of NAT ;

        consider g such that

         A3: P[t, g] by A1;

        reconsider g as Element of COMPLEX by XCMPLX_0:def 2;

        take g;

        thus P[t, g] by A3;

      end;

      consider f be sequence of COMPLEX such that

       A4: for t be Element of NAT holds P[t, (f . t)] from FUNCT_2:sch 3( A2);

      reconsider s = f as Complex_Sequence;

      take s;

      let n;

      n in NAT by ORDINAL1:def 12;

      hence thesis by A4;

    end;

    begin

    theorem :: CFCONT_1:31

    f is_continuous_in x0 iff x0 in ( dom f) & for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1))

    proof

      thus f is_continuous_in x0 implies x0 in ( dom f) & for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

      assume that

       A1: x0 in ( dom f) and

       A2: for s1 st ( rng s1) c= ( dom f) & s1 is convergent & ( lim s1) = x0 & (for n holds (s1 . n) <> x0) holds (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1));

      thus x0 in ( dom f) by A1;

      let s2 such that

       A3: ( rng s2) c= ( dom f) and

       A4: s2 is convergent & ( lim s2) = x0;

      now

        per cases ;

          suppose ex n st for m st n <= m holds (s2 . m) = x0;

          then

          consider N be Nat such that

           A5: for m st N <= m holds (s2 . m) = x0;

          

           A6: for n holds ((s2 ^\ N) . n) = x0

          proof

            let n;

            (s2 . (n + N)) = x0 by A5, NAT_1: 12;

            hence thesis by NAT_1:def 3;

          end;

          

           A7: (f /* (s2 ^\ N)) = ((f /* s2) ^\ N) by A3, VALUED_0: 27;

          

           A8: ( rng (s2 ^\ N)) c= ( rng s2) by VALUED_0: 21;

           A9:

          now

            let p such that

             A10: p > 0 ;

            reconsider n = 0 as Nat;

            take n;

            let m such that n <= m;

            m in NAT by ORDINAL1:def 12;

            

            then |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| = |.((f /. ((s2 ^\ N) . m)) - (f /. x0)).| by A3, A8, FUNCT_2: 109, XBOOLE_1: 1

            .= |.((f /. x0) - (f /. x0)).| by A6

            .= 0 by COMPLEX1: 44;

            hence |.(((f /* (s2 ^\ N)) . m) - (f /. x0)).| < p by A10;

          end;

          then

           A11: (f /* (s2 ^\ N)) is convergent;

          then (f /. x0) = ( lim ((f /* s2) ^\ N)) by A9, A7, COMSEQ_2:def 6;

          hence thesis by A11, A7, Th18, Th22;

        end;

          suppose

           A12: for n holds ex m st n <= m & (s2 . m) <> x0;

          defpred P2[ set, set] means for n, m st $1 = n & $2 = m holds n < m & (s2 . m) <> x0 & for k st n < k & (s2 . k) <> x0 holds m <= k;

          defpred R[ set, set, set] means P2[$2, $3];

          defpred P[ set] means (s2 . $1) <> x0;

          ex m1 be Nat st 0 <= m1 & (s2 . m1) <> x0 by A12;

          then

           A13: ex m be Nat st P[m];

          consider M be Nat such that

           A14: P[M] & for n be Nat st P[n] holds M <= n from NAT_1:sch 5( A13);

          reconsider M9 = M as Element of NAT by ORDINAL1:def 12;

           A15:

          now

            let n;

            consider m such that

             A16: (n + 1) <= m & (s2 . m) <> x0 by A12;

            take m;

            thus n < m & (s2 . m) <> x0 by A16, NAT_1: 13;

          end;

          

           A17: for n be Nat holds for x be Element of NAT holds ex y be Element of NAT st R[n, x, y]

          proof

            let n be Nat;

            let x be Element of NAT ;

            defpred P[ Nat] means x < $1 & (s2 . $1) <> x0;

            ex m st P[m] by A15;

            then

             A18: ex m be Nat st P[m];

            consider l be Nat such that

             A19: P[l] & for k be Nat st P[k] holds l <= k from NAT_1:sch 5( A18);

            take l;

            l in NAT by ORDINAL1:def 12;

            hence thesis by A19;

          end;

          consider F be sequence of NAT such that

           A20: (F . 0 ) = M9 & for n be Nat holds R[n, (F . n), (F . (n + 1))] from RECDEF_1:sch 2( A17);

          

           A21: for n holds (F . n) is real;

          ( dom F) = NAT by FUNCT_2:def 1;

          then

          reconsider F as Real_Sequence by A21, SEQ_1: 2;

          for n holds (F . n) < (F . (n + 1)) by A20;

          then

          reconsider F as increasing sequence of NAT by SEQM_3:def 6;

          

           A22: (s2 * F) is subsequence of s2 by VALUED_0:def 17;

          then

           A23: (s2 * F) is convergent & ( lim (s2 * F)) = x0 by A4, Th17, Th18;

          

           A24: for n st (s2 . n) <> x0 holds ex m st (F . m) = n

          proof

            defpred P[ set] means (s2 . $1) <> x0 & for m holds (F . m) <> $1;

            assume ex n st P[n];

            then

             A25: ex n be Nat st P[n];

            consider M1 be Nat such that

             A26: P[M1] & for n be Nat st P[n] holds M1 <= n from NAT_1:sch 5( A25);

            defpred E[ Nat] means $1 < M1 & (s2 . $1) <> x0 & ex m st (F . m) = $1;

            

             A27: ex n be Nat st E[n]

            proof

              take M;

              M <= M1 & M <> M1 by A14, A20, A26;

              hence M < M1 by XXREAL_0: 1;

              thus (s2 . M) <> x0 by A14;

              take 0 ;

              thus thesis by A20;

            end;

            

             A28: for n be Nat st E[n] holds n <= M1;

            consider MX be Nat such that

             A29: E[MX] & for n be Nat st E[n] holds n <= MX from NAT_1:sch 6( A28, A27);

            

             A30: for k st MX < k & k < M1 holds (s2 . k) = x0

            proof

              given k such that

               A31: MX < k and

               A32: k < M1 & (s2 . k) <> x0;

              now

                per cases ;

                  suppose ex m st (F . m) = k;

                  hence contradiction by A29, A31, A32;

                end;

                  suppose for m holds (F . m) <> k;

                  hence contradiction by A26, A32;

                end;

              end;

              hence contradiction;

            end;

            consider m such that

             A33: (F . m) = MX by A29;

            

             A34: MX < (F . (m + 1)) & (s2 . (F . (m + 1))) <> x0 by A20, A33;

            

             A35: (F . (m + 1)) <= M1 by A20, A26, A29, A33;

            now

              assume (F . (m + 1)) <> M1;

              then (F . (m + 1)) < M1 by A35, XXREAL_0: 1;

              hence contradiction by A30, A34;

            end;

            hence contradiction by A26;

          end;

          defpred P[ Nat] means ((s2 * F) . $1) <> x0;

          

           A36: for k st P[k] holds P[(k + 1)]

          proof

            let k such that ((s2 * F) . k) <> x0;

             P2[(F . k), (F . (k + 1))] by A20;

            then (s2 . (F . (k + 1))) <> x0;

            hence thesis by FUNCT_2: 15;

          end;

          

           A37: P[ 0 ] by A14, A20, FUNCT_2: 15;

          

           A38: for n holds P[n] from NAT_1:sch 2( A37, A36);

          

           A39: ( rng (s2 * F)) c= ( rng s2) by A22, VALUED_0: 21;

          then ( rng (s2 * F)) c= ( dom f) by A3;

          then

           A40: (f /* (s2 * F)) is convergent & (f /. x0) = ( lim (f /* (s2 * F))) by A2, A38, A23;

           A41:

          now

            let p;

            assume

             A42: 0 < p;

            then

            consider n such that

             A43: for m st n <= m holds |.(((f /* (s2 * F)) . m) - (f /. x0)).| < p by A40, COMSEQ_2:def 6;

            reconsider k = (F . n) as Nat;

            take k;

            let m such that

             A44: k <= m;

            per cases ;

              suppose

               A45: (s2 . m) = x0;

              m in NAT by ORDINAL1:def 12;

              

              then |.(((f /* s2) . m) - (f /. x0)).| = |.((f /. x0) - (f /. x0)).| by A3, FUNCT_2: 109, A45

              .= 0 by COMPLEX1: 44;

              hence |.(((f /* s2) . m) - (f /. x0)).| < p by A42;

            end;

              suppose (s2 . m) <> x0;

              then

              consider l be Nat such that

               A46: m = (F . l) by A24;

              

               A47: l in NAT by ORDINAL1:def 12;

              

               A48: m in NAT by ORDINAL1:def 12;

              n <= l by A44, A46, SEQM_3: 1;

              then |.(((f /* (s2 * F)) . l) - (f /. x0)).| < p by A43;

              then |.((f /. ((s2 * F) . l)) - (f /. x0)).| < p by A3, A39, FUNCT_2: 109, XBOOLE_1: 1, A47;

              then |.((f /. (s2 . m)) - (f /. x0)).| < p by A46, FUNCT_2: 15, A47;

              hence |.(((f /* s2) . m) - (f /. x0)).| < p by A3, FUNCT_2: 109, A48;

            end;

          end;

          hence (f /* s2) is convergent;

          hence (f /. x0) = ( lim (f /* s2)) by A41, COMSEQ_2:def 6;

        end;

      end;

      hence thesis;

    end;

    theorem :: CFCONT_1:32

    

     Th32: f is_continuous_in x0 iff x0 in ( dom f) & for r st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

    proof

      thus f is_continuous_in x0 implies x0 in ( dom f) & for r st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

      proof

        assume

         A1: f is_continuous_in x0;

        hence x0 in ( dom f);

        given r such that

         A2: 0 < r and

         A3: for s holds not 0 < s or ex x1 st x1 in ( dom f) & |.(x1 - x0).| < s & not |.((f /. x1) - (f /. x0)).| < r;

        defpred P[ Nat, Complex] means $2 in ( dom f) & |.($2 - x0).| < (1 / ($1 + 1)) & not |.((f /. $2) - (f /. x0)).| < r;

        

         A4: for n holds ex g st P[n, g]

        proof

          let n;

           0 < (1 / (n + 1));

          then

          consider g such that

           A5: g in ( dom f) & |.(g - x0).| < (1 / (n + 1)) & not |.((f /. g) - (f /. x0)).| < r by A3;

          take g;

          thus thesis by A5;

        end;

        consider s1 such that

         A6: for n holds P[n, (s1 . n)] from CompSeqChoice( A4);

        

         A7: ( rng s1) c= ( dom f)

        proof

          let x be object;

          assume x in ( rng s1);

          then ex n be Element of NAT st x = (s1 . n) by FUNCT_2: 113;

          hence thesis by A6;

        end;

         A8:

        now

          let n;

          

           A9: n in NAT by ORDINAL1:def 12;

           not |.((f /. (s1 . n)) - (f /. x0)).| < r by A6;

          hence not |.(((f /* s1) . n) - (f /. x0)).| < r by A7, FUNCT_2: 109, A9;

        end;

         A10:

        now

          let s;

          consider n such that

           A11: (s " ) < n by SEQ_4: 3;

          assume 0 < s;

          then

           A12: 0 < (s " );

          ((s " ) + 0 ) < (n + 1) by A11, XREAL_1: 8;

          then (1 / (n + 1)) < (1 / (s " )) by A12, XREAL_1: 76;

          then

           A13: (1 / (n + 1)) < s by XCMPLX_1: 216;

          take k = n;

          let m;

          assume k <= m;

          then (k + 1) <= (m + 1) by XREAL_1: 6;

          then (1 / (m + 1)) <= (1 / (k + 1)) by XREAL_1: 118;

          then (1 / (m + 1)) < s by A13, XXREAL_0: 2;

          hence |.((s1 . m) - x0).| < s by A6, XXREAL_0: 2;

        end;

        then

         A14: s1 is convergent;

        then ( lim s1) = x0 by A10, COMSEQ_2:def 6;

        then (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1)) by A1, A7, A14;

        then

        consider n such that

         A15: for m st n <= m holds |.(((f /* s1) . m) - (f /. x0)).| < r by A2, COMSEQ_2:def 6;

         |.(((f /* s1) . n) - (f /. x0)).| < r by A15;

        hence contradiction by A8;

      end;

      assume that

       A16: x0 in ( dom f) and

       A17: for r st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r;

      now

        let s1 such that

         A18: ( rng s1) c= ( dom f) and

         A19: s1 is convergent & ( lim s1) = x0;

         A20:

        now

          let p;

          assume 0 < p;

          then

          consider s such that

           A21: 0 < s and

           A22: for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < p by A17;

          consider n such that

           A23: for m st n <= m holds |.((s1 . m) - x0).| < s by A19, A21, COMSEQ_2:def 6;

          take k = n;

          let m;

          

           A24: m in NAT by ORDINAL1:def 12;

          assume k <= m;

          then (s1 . m) in ( rng s1) & |.((s1 . m) - x0).| < s by A23, VALUED_0: 28;

          then |.((f /. (s1 . m)) - (f /. x0)).| < p by A18, A22;

          hence |.(((f /* s1) . m) - (f /. x0)).| < p by A18, FUNCT_2: 109, A24;

        end;

        then (f /* s1) is convergent;

        hence (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1)) by A20, COMSEQ_2:def 6;

      end;

      hence thesis by A16;

    end;

    theorem :: CFCONT_1:33

    

     Th33: f1 is_continuous_in x0 & f2 is_continuous_in x0 implies (f1 + f2) is_continuous_in x0 & (f1 - f2) is_continuous_in x0 & (f1 (#) f2) is_continuous_in x0

    proof

      assume that

       A1: f1 is_continuous_in x0 and

       A2: f2 is_continuous_in x0;

      

       A3: x0 in ( dom f1) & x0 in ( dom f2) by A1, A2;

      now

        x0 in (( dom f1) /\ ( dom f2)) by A3, XBOOLE_0:def 4;

        hence

         A4: x0 in ( dom (f1 + f2)) by VALUED_1:def 1;

        let s1;

        assume that

         A5: ( rng s1) c= ( dom (f1 + f2)) and

         A6: s1 is convergent & ( lim s1) = x0;

        

         A7: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A5, VALUED_1:def 1;

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

        then ( dom (f1 + f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A8: ( rng s1) c= ( dom f2) by A5;

        then

         A9: (f2 /* s1) is convergent by A2, A6;

        ( dom (f1 + f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 1;

        then ( dom (f1 + f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A10: ( rng s1) c= ( dom f1) by A5;

        then

         A11: (f1 /* s1) is convergent by A1, A6;

        then ((f1 /* s1) + (f2 /* s1)) is convergent by A9;

        hence ((f1 + f2) /* s1) is convergent by A7, Th7;

        

         A12: (f1 /. x0) = ( lim (f1 /* s1)) by A1, A6, A10;

        

         A13: (f2 /. x0) = ( lim (f2 /* s1)) by A2, A6, A8;

        

        thus ((f1 + f2) /. x0) = ((f1 /. x0) + (f2 /. x0)) by A4, CFUNCT_1: 1

        .= ( lim ((f1 /* s1) + (f2 /* s1))) by A11, A12, A9, A13, COMSEQ_2: 14

        .= ( lim ((f1 + f2) /* s1)) by A7, Th7;

      end;

      hence (f1 + f2) is_continuous_in x0;

      now

        x0 in (( dom f1) /\ ( dom f2)) by A3, XBOOLE_0:def 4;

        hence

         A14: x0 in ( dom (f1 - f2)) by CFUNCT_1: 2;

        let s1;

        assume that

         A15: ( rng s1) c= ( dom (f1 - f2)) and

         A16: s1 is convergent & ( lim s1) = x0;

        

         A17: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A15, CFUNCT_1: 2;

        ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by CFUNCT_1: 2;

        then ( dom (f1 - f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A18: ( rng s1) c= ( dom f2) by A15;

        then

         A19: (f2 /* s1) is convergent by A2, A16;

        ( dom (f1 - f2)) = (( dom f1) /\ ( dom f2)) by CFUNCT_1: 2;

        then ( dom (f1 - f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A20: ( rng s1) c= ( dom f1) by A15;

        then

         A21: (f1 /* s1) is convergent by A1, A16;

        then ((f1 /* s1) - (f2 /* s1)) is convergent by A19;

        hence ((f1 - f2) /* s1) is convergent by A17, Th7;

        

         A22: (f1 /. x0) = ( lim (f1 /* s1)) by A1, A16, A20;

        

         A23: (f2 /. x0) = ( lim (f2 /* s1)) by A2, A16, A18;

        

        thus ((f1 - f2) /. x0) = ((f1 /. x0) - (f2 /. x0)) by A14, CFUNCT_1: 2

        .= ( lim ((f1 /* s1) - (f2 /* s1))) by A21, A22, A19, A23, COMSEQ_2: 26

        .= ( lim ((f1 - f2) /* s1)) by A17, Th7;

      end;

      hence (f1 - f2) is_continuous_in x0;

      x0 in (( dom f1) /\ ( dom f2)) by A3, XBOOLE_0:def 4;

      hence

       A24: x0 in ( dom (f1 (#) f2)) by VALUED_1:def 4;

      let s1;

      assume that

       A25: ( rng s1) c= ( dom (f1 (#) f2)) and

       A26: s1 is convergent & ( lim s1) = x0;

      ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

      then ( dom (f1 (#) f2)) c= ( dom f2) by XBOOLE_1: 17;

      then

       A27: ( rng s1) c= ( dom f2) by A25;

      then

       A28: (f2 /* s1) is convergent by A2, A26;

      

       A29: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A25, VALUED_1:def 4;

      ( dom (f1 (#) f2)) = (( dom f1) /\ ( dom f2)) by VALUED_1:def 4;

      then ( dom (f1 (#) f2)) c= ( dom f1) by XBOOLE_1: 17;

      then

       A30: ( rng s1) c= ( dom f1) by A25;

      then

       A31: (f1 /* s1) is convergent by A1, A26;

      then ((f1 /* s1) (#) (f2 /* s1)) is convergent by A28;

      hence ((f1 (#) f2) /* s1) is convergent by A29, Th7;

      

       A32: (f1 /. x0) = ( lim (f1 /* s1)) by A1, A26, A30;

      

       A33: (f2 /. x0) = ( lim (f2 /* s1)) by A2, A26, A27;

      

      thus ((f1 (#) f2) /. x0) = ((f1 /. x0) * (f2 /. x0)) by A24, CFUNCT_1: 3

      .= ( lim ((f1 /* s1) (#) (f2 /* s1))) by A31, A32, A28, A33, COMSEQ_2: 30

      .= ( lim ((f1 (#) f2) /* s1)) by A29, Th7;

    end;

    theorem :: CFCONT_1:34

    

     Th34: f is_continuous_in x0 implies (g (#) f) is_continuous_in x0

    proof

      assume

       A1: f is_continuous_in x0;

      then x0 in ( dom f);

      hence

       A2: x0 in ( dom (g (#) f)) by VALUED_1:def 5;

      let s1;

      assume that

       A3: ( rng s1) c= ( dom (g (#) f)) and

       A4: s1 is convergent & ( lim s1) = x0;

      

       A5: ( rng s1) c= ( dom f) by A3, VALUED_1:def 5;

      then

       A6: (f /. x0) = ( lim (f /* s1)) by A1, A4;

      

       A7: (f /* s1) is convergent by A1, A4, A5;

      then (g (#) (f /* s1)) is convergent;

      hence ((g (#) f) /* s1) is convergent by A5, Th8;

      

      thus ((g (#) f) /. x0) = (g * (f /. x0)) by A2, CFUNCT_1: 4

      .= ( lim (g (#) (f /* s1))) by A7, A6, COMSEQ_2: 18

      .= ( lim ((g (#) f) /* s1)) by A5, Th8;

    end;

    theorem :: CFCONT_1:35

    f is_continuous_in x0 implies ( - f) is_continuous_in x0 by Th34;

    theorem :: CFCONT_1:36

    

     Th36: f is_continuous_in x0 & (f /. x0) <> 0 implies (f ^ ) is_continuous_in x0

    proof

      assume that

       A1: f is_continuous_in x0 and

       A2: (f /. x0) <> 0 ;

       not (f /. x0) in { 0c } by A2, TARSKI:def 1;

      then

       A3: not x0 in (f " { 0c }) by PARTFUN2: 26;

      x0 in ( dom f) by A1;

      then x0 in (( dom f) \ (f " { 0c })) by A3, XBOOLE_0:def 5;

      hence

       A4: x0 in ( dom (f ^ )) by CFUNCT_1:def 2;

      let s1;

      assume that

       A5: ( rng s1) c= ( dom (f ^ )) and

       A6: s1 is convergent & ( lim s1) = x0;

      (( dom f) \ (f " { 0c })) c= ( dom f) & ( rng s1) c= (( dom f) \ (f " { 0c })) by A5, CFUNCT_1:def 2, XBOOLE_1: 36;

      then ( rng s1) c= ( dom f);

      then

       A7: (f /* s1) is convergent & (f /. x0) = ( lim (f /* s1)) by A1, A6;

      (f /* s1) is non-zero by A5, Th10;

      then ((f /* s1) " ) is convergent by A2, A7, COMSEQ_2: 34;

      hence ((f ^ ) /* s1) is convergent by A5, Th11;

      

      thus ((f ^ ) /. x0) = ((f /. x0) " ) by A4, CFUNCT_1:def 2

      .= ( lim ((f /* s1) " )) by A2, A5, A7, Th10, COMSEQ_2: 35

      .= ( lim ((f ^ ) /* s1)) by A5, Th11;

    end;

    theorem :: CFCONT_1:37

    f1 is_continuous_in x0 & (f1 /. x0) <> 0 & f2 is_continuous_in x0 implies (f2 / f1) is_continuous_in x0

    proof

      assume that

       A1: f1 is_continuous_in x0 & (f1 /. x0) <> 0 and

       A2: f2 is_continuous_in x0;

      (f1 ^ ) is_continuous_in x0 by A1, Th36;

      then (f2 (#) (f1 ^ )) is_continuous_in x0 by A2, Th33;

      hence thesis by CFUNCT_1: 39;

    end;

    definition

      let f, X;

      :: CFCONT_1:def2

      pred f is_continuous_on X means X c= ( dom f) & for x0 st x0 in X holds (f | X) is_continuous_in x0;

    end

    theorem :: CFCONT_1:38

    

     Th38: for X, f holds f is_continuous_on X iff X c= ( dom f) & for s1 st ( rng s1) c= X & s1 is convergent & ( lim s1) in X holds (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1))

    proof

      let X, f;

      thus f is_continuous_on X implies X c= ( dom f) & for s1 st ( rng s1) c= X & s1 is convergent & ( lim s1) in X holds (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1))

      proof

        assume

         A1: f is_continuous_on X;

        then

         A2: X c= ( dom f);

        now

          let s1 such that

           A3: ( rng s1) c= X and

           A4: s1 is convergent and

           A5: ( lim s1) in X;

          

           A6: (f | X) is_continuous_in ( lim s1) by A1, A5;

          

           A7: ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61

          .= X by A2, XBOOLE_1: 28;

          now

            let n be Element of NAT ;

            

             A8: (s1 . n) in ( rng s1) by VALUED_0: 28;

            

            thus (((f | X) /* s1) . n) = ((f | X) /. (s1 . n)) by A3, A7, FUNCT_2: 109

            .= (f /. (s1 . n)) by A3, A7, A8, PARTFUN2: 15

            .= ((f /* s1) . n) by A2, A3, FUNCT_2: 109, XBOOLE_1: 1;

          end;

          then

           A9: ((f | X) /* s1) = (f /* s1) by FUNCT_2: 63;

          (f /. ( lim s1)) = ((f | X) /. ( lim s1)) by A5, A7, PARTFUN2: 15

          .= ( lim (f /* s1)) by A3, A4, A7, A6, A9;

          hence (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1)) by A3, A4, A7, A6, A9;

        end;

        hence thesis by A1;

      end;

      assume that

       A10: X c= ( dom f) and

       A11: for s1 st ( rng s1) c= X & s1 is convergent & ( lim s1) in X holds (f /* s1) is convergent & (f /. ( lim s1)) = ( lim (f /* s1));

      now

        

         A12: ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61

        .= X by A10, XBOOLE_1: 28;

        let x1 such that

         A13: x1 in X;

        now

          let s1 such that

           A14: ( rng s1) c= ( dom (f | X)) and

           A15: s1 is convergent and

           A16: ( lim s1) = x1;

          now

            let n be Element of NAT ;

            

             A17: (s1 . n) in ( rng s1) by VALUED_0: 28;

            

            thus (((f | X) /* s1) . n) = ((f | X) /. (s1 . n)) by A14, FUNCT_2: 109

            .= (f /. (s1 . n)) by A14, A17, PARTFUN2: 15

            .= ((f /* s1) . n) by A10, A12, A14, FUNCT_2: 109, XBOOLE_1: 1;

          end;

          then

           A18: ((f | X) /* s1) = (f /* s1) by FUNCT_2: 63;

          ((f | X) /. ( lim s1)) = (f /. ( lim s1)) by A13, A12, A16, PARTFUN2: 15

          .= ( lim ((f | X) /* s1)) by A11, A13, A12, A14, A15, A16, A18;

          hence ((f | X) /* s1) is convergent & ((f | X) /. x1) = ( lim ((f | X) /* s1)) by A11, A13, A12, A14, A15, A16, A18;

        end;

        hence (f | X) is_continuous_in x1 by A13, A12;

      end;

      hence thesis by A10;

    end;

    theorem :: CFCONT_1:39

    

     Th39: f is_continuous_on X iff X c= ( dom f) & for x0, r st x0 in X & 0 < r holds ex s st 0 < s & for x1 st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

    proof

      thus f is_continuous_on X implies X c= ( dom f) & for x0, r st x0 in X & 0 < r holds ex s st 0 < s & for x1 st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r

      proof

        assume

         A1: f is_continuous_on X;

        hence X c= ( dom f);

        

         A2: X c= ( dom f) by A1;

        let x0, r;

        assume that

         A3: x0 in X and

         A4: 0 < r;

        (f | X) is_continuous_in x0 by A1, A3;

        then

        consider s such that

         A5: 0 < s and

         A6: for x1 st x1 in ( dom (f | X)) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A4, Th32;

        take s;

        thus 0 < s by A5;

        let x1;

        assume that

         A7: x1 in X and

         A8: |.(x1 - x0).| < s;

        

         A9: ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61

        .= X by A2, XBOOLE_1: 28;

        

        then |.((f /. x1) - (f /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A7, PARTFUN2: 15

        .= |.(((f | X) /. x1) - ((f | X) /. x0)).| by A3, A9, PARTFUN2: 15;

        hence thesis by A6, A9, A7, A8;

      end;

      assume that

       A10: X c= ( dom f) and

       A11: for x0, r st x0 in X & 0 < r holds ex s st 0 < s & for x1 st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r;

      

       A12: ( dom (f | X)) = (( dom f) /\ X) by RELAT_1: 61

      .= X by A10, XBOOLE_1: 28;

      now

        let x0 such that

         A13: x0 in X;

        for r st 0 < r holds ex s st 0 < s & for x1 st x1 in ( dom (f | X)) & |.(x1 - x0).| < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r

        proof

          let r;

          assume 0 < r;

          then

          consider s such that

           A14: 0 < s and

           A15: for x1 st x1 in X & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r by A11, A13;

          take s;

          thus 0 < s by A14;

          let x1 such that

           A16: x1 in ( dom (f | X)) and

           A17: |.(x1 - x0).| < s;

           |.(((f | X) /. x1) - ((f | X) /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A12, A13, PARTFUN2: 15

          .= |.((f /. x1) - (f /. x0)).| by A16, PARTFUN2: 15;

          hence thesis by A12, A15, A16, A17;

        end;

        hence (f | X) is_continuous_in x0 by A12, A13, Th32;

      end;

      hence thesis by A10;

    end;

    theorem :: CFCONT_1:40

    

     Th40: f is_continuous_on X iff (f | X) is_continuous_on X

    proof

      thus f is_continuous_on X implies (f | X) is_continuous_on X

      proof

        assume

         A1: f is_continuous_on X;

        then X c= ( dom f);

        then X c= (( dom f) /\ X) by XBOOLE_1: 28;

        hence X c= ( dom (f | X)) by RELAT_1: 61;

        let g;

        assume g in X;

        then (f | X) is_continuous_in g by A1;

        hence thesis by RELAT_1: 72;

      end;

      assume

       A2: (f | X) is_continuous_on X;

      then X c= ( dom (f | X));

      then (( dom f) /\ X) c= ( dom f) & X c= (( dom f) /\ X) by RELAT_1: 61, XBOOLE_1: 17;

      hence X c= ( dom f);

      let g;

      assume g in X;

      then ((f | X) | X) is_continuous_in g by A2;

      hence thesis by RELAT_1: 72;

    end;

    theorem :: CFCONT_1:41

    

     Th41: f is_continuous_on X & X1 c= X implies f is_continuous_on X1

    proof

      assume that

       A1: f is_continuous_on X and

       A2: X1 c= X;

      X c= ( dom f) by A1;

      hence

       A3: X1 c= ( dom f) by A2;

      let g;

      assume

       A4: g in X1;

      then

       A5: (f | X) is_continuous_in g by A1, A2;

      thus (f | X1) is_continuous_in g

      proof

        (( dom f) /\ X1) c= (( dom f) /\ X) by A2, XBOOLE_1: 26;

        then ( dom (f | X1)) c= (( dom f) /\ X) by RELAT_1: 61;

        then

         A6: ( dom (f | X1)) c= ( dom (f | X)) by RELAT_1: 61;

        g in (( dom f) /\ X1) by A3, A4, XBOOLE_0:def 4;

        hence

         A7: g in ( dom (f | X1)) by RELAT_1: 61;

        

        then

         A8: ((f | X) /. g) = (f /. g) by A6, PARTFUN2: 15

        .= ((f | X1) /. g) by A7, PARTFUN2: 15;

        let s1 such that

         A9: ( rng s1) c= ( dom (f | X1)) and

         A10: s1 is convergent & ( lim s1) = g;

        

         A11: ( rng s1) c= ( dom (f | X)) by A9, A6;

         A12:

        now

          let n be Element of NAT ;

          

           A13: (s1 . n) in ( rng s1) by VALUED_0: 28;

          

          thus (((f | X) /* s1) . n) = ((f | X) /. (s1 . n)) by A9, A6, FUNCT_2: 109, XBOOLE_1: 1

          .= (f /. (s1 . n)) by A11, A13, PARTFUN2: 15

          .= ((f | X1) /. (s1 . n)) by A9, A13, PARTFUN2: 15

          .= (((f | X1) /* s1) . n) by A9, FUNCT_2: 109;

        end;

        ((f | X) /* s1) is convergent & ((f | X) /. g) = ( lim ((f | X) /* s1)) by A5, A10, A11;

        hence thesis by A8, A12, FUNCT_2: 63;

      end;

    end;

    theorem :: CFCONT_1:42

    x0 in ( dom f) implies f is_continuous_on {x0}

    proof

      assume

       A1: x0 in ( dom f);

      thus {x0} c= ( dom f) by A1, TARSKI:def 1;

      let t such that

       A2: t in {x0};

      thus (f | {x0}) is_continuous_in t

      proof

        t in ( dom f) by A1, A2, TARSKI:def 1;

        then t in (( dom f) /\ {x0}) by A2, XBOOLE_0:def 4;

        hence t in ( dom (f | {x0})) by RELAT_1: 61;

        let s1;

        assume that

         A3: ( rng s1) c= ( dom (f | {x0})) and s1 is convergent and ( lim s1) = t;

        

         A4: (( dom f) /\ {x0}) c= {x0} by XBOOLE_1: 17;

        ( rng s1) c= (( dom f) /\ {x0}) by A3, RELAT_1: 61;

        then

         A5: ( rng s1) c= {x0} by A4;

         A6:

        now

          let n;

          (s1 . n) in ( rng s1) by VALUED_0: 28;

          hence (s1 . n) = x0 by A5, TARSKI:def 1;

        end;

        

         A7: t = x0 by A2, TARSKI:def 1;

         A8:

        now

          let r such that

           A9: 0 < r;

          reconsider n = 0 as Nat;

          take n;

          let m such that n <= m;

          

           A10: m in NAT by ORDINAL1:def 12;

           |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| = |.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).| by A7, A3, FUNCT_2: 109, A10

          .= |.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).| by A6

          .= 0 by COMPLEX1: 44;

          hence |.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. t)).| < r by A9;

        end;

        hence ((f | {x0}) /* s1) is convergent;

        hence thesis by A8, COMSEQ_2:def 6;

      end;

    end;

    theorem :: CFCONT_1:43

    

     Th43: for X, f1, f2 st f1 is_continuous_on X & f2 is_continuous_on X holds (f1 + f2) is_continuous_on X & (f1 - f2) is_continuous_on X & (f1 (#) f2) is_continuous_on X

    proof

      let X, f1, f2;

      assume

       A1: f1 is_continuous_on X & f2 is_continuous_on X;

      then X c= ( dom f1) & X c= ( dom f2);

      then

       A2: X c= (( dom f1) /\ ( dom f2)) by XBOOLE_1: 19;

      then

       A3: X c= ( dom (f1 + f2)) by CFUNCT_1: 1;

      now

        let s1;

        assume that

         A4: ( rng s1) c= X and

         A5: s1 is convergent and

         A6: ( lim s1) in X;

        

         A7: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A1, A4, A5, A6, Th38;

        then

         A8: ((f1 /* s1) + (f2 /* s1)) is convergent;

        

         A9: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A2, A4;

        

         A10: ( lim s1) in ( dom (f1 + f2)) by A3, A6;

        (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A1, A4, A5, A6, Th38;

        

        then ((f1 + f2) /. ( lim s1)) = (( lim (f1 /* s1)) + ( lim (f2 /* s1))) by A10, CFUNCT_1: 1

        .= ( lim ((f1 /* s1) + (f2 /* s1))) by A7, COMSEQ_2: 14

        .= ( lim ((f1 + f2) /* s1)) by A9, Th7;

        hence ((f1 + f2) /* s1) is convergent & ((f1 + f2) /. ( lim s1)) = ( lim ((f1 + f2) /* s1)) by A9, A8, Th7;

      end;

      hence (f1 + f2) is_continuous_on X by A3, Th38;

      

       A11: X c= ( dom (f1 - f2)) by A2, CFUNCT_1: 2;

      now

        let s1;

        assume that

         A12: ( rng s1) c= X and

         A13: s1 is convergent and

         A14: ( lim s1) in X;

        

         A15: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A1, A12, A13, A14, Th38;

        then

         A16: ((f1 /* s1) - (f2 /* s1)) is convergent;

        

         A17: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A2, A12;

        

         A18: ( lim s1) in ( dom (f1 - f2)) by A11, A14;

        (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A1, A12, A13, A14, Th38;

        

        then ((f1 - f2) /. ( lim s1)) = (( lim (f1 /* s1)) - ( lim (f2 /* s1))) by A18, CFUNCT_1: 2

        .= ( lim ((f1 /* s1) - (f2 /* s1))) by A15, COMSEQ_2: 26

        .= ( lim ((f1 - f2) /* s1)) by A17, Th7;

        hence ((f1 - f2) /* s1) is convergent & ((f1 - f2) /. ( lim s1)) = ( lim ((f1 - f2) /* s1)) by A17, A16, Th7;

      end;

      hence (f1 - f2) is_continuous_on X by A11, Th38;

      

       A19: X c= ( dom (f1 (#) f2)) by A2, CFUNCT_1: 3;

      now

        let s1;

        assume that

         A20: ( rng s1) c= X and

         A21: s1 is convergent and

         A22: ( lim s1) in X;

        

         A23: (f1 /* s1) is convergent & (f2 /* s1) is convergent by A1, A20, A21, A22, Th38;

        then

         A24: ((f1 /* s1) (#) (f2 /* s1)) is convergent;

        

         A25: ( rng s1) c= (( dom f1) /\ ( dom f2)) by A2, A20;

        

         A26: ( lim s1) in ( dom (f1 (#) f2)) by A19, A22;

        (f1 /. ( lim s1)) = ( lim (f1 /* s1)) & (f2 /. ( lim s1)) = ( lim (f2 /* s1)) by A1, A20, A21, A22, Th38;

        

        then ((f1 (#) f2) /. ( lim s1)) = (( lim (f1 /* s1)) * ( lim (f2 /* s1))) by A26, CFUNCT_1: 3

        .= ( lim ((f1 /* s1) (#) (f2 /* s1))) by A23, COMSEQ_2: 30

        .= ( lim ((f1 (#) f2) /* s1)) by A25, Th7;

        hence ((f1 (#) f2) /* s1) is convergent & ((f1 (#) f2) /. ( lim s1)) = ( lim ((f1 (#) f2) /* s1)) by A25, A24, Th7;

      end;

      hence thesis by A19, Th38;

    end;

    theorem :: CFCONT_1:44

    for X, X1, f1, f2 st f1 is_continuous_on X & f2 is_continuous_on X1 holds (f1 + f2) is_continuous_on (X /\ X1) & (f1 - f2) is_continuous_on (X /\ X1) & (f1 (#) f2) is_continuous_on (X /\ X1)

    proof

      let X, X1, f1, f2;

      assume f1 is_continuous_on X & f2 is_continuous_on X1;

      then f1 is_continuous_on (X /\ X1) & f2 is_continuous_on (X /\ X1) by Th41, XBOOLE_1: 17;

      hence thesis by Th43;

    end;

    theorem :: CFCONT_1:45

    

     Th45: for g, X, f st f is_continuous_on X holds (g (#) f) is_continuous_on X

    proof

      let g, X, f;

      assume

       A1: f is_continuous_on X;

      then

       A2: X c= ( dom f);

      then

       A3: X c= ( dom (g (#) f)) by CFUNCT_1: 4;

      now

        let s1;

        assume that

         A4: ( rng s1) c= X and

         A5: s1 is convergent and

         A6: ( lim s1) in X;

        

         A7: (f /* s1) is convergent by A1, A4, A5, A6, Th38;

        then

         A8: (g (#) (f /* s1)) is convergent;

        

         A9: ( lim s1) in ( dom (g (#) f)) by A3, A6;

        (f /. ( lim s1)) = ( lim (f /* s1)) by A1, A4, A5, A6, Th38;

        

        then ((g (#) f) /. ( lim s1)) = (g * ( lim (f /* s1))) by CFUNCT_1: 4, A9

        .= ( lim (g (#) (f /* s1))) by A7, COMSEQ_2: 18

        .= ( lim ((g (#) f) /* s1)) by A2, A4, Th8, XBOOLE_1: 1;

        hence ((g (#) f) /* s1) is convergent & ((g (#) f) /. ( lim s1)) = ( lim ((g (#) f) /* s1)) by A2, A4, A8, Th8, XBOOLE_1: 1;

      end;

      hence thesis by A3, Th38;

    end;

    theorem :: CFCONT_1:46

    f is_continuous_on X implies ( - f) is_continuous_on X by Th45;

    theorem :: CFCONT_1:47

    

     Th47: f is_continuous_on X & (f " { 0 }) = {} implies (f ^ ) is_continuous_on X

    proof

      assume that

       A1: f is_continuous_on X and

       A2: (f " { 0 }) = {} ;

      

       A3: ( dom (f ^ )) = (( dom f) \ {} ) by A2, CFUNCT_1:def 2

      .= ( dom f);

      hence

       A4: X c= ( dom (f ^ )) by A1;

      let g;

      assume

       A5: g in X;

      then

       A6: (f | X) is_continuous_in g by A1;

      g in (( dom (f ^ )) /\ X) by A4, A5, XBOOLE_0:def 4;

      then

       A7: g in ( dom ((f ^ ) | X)) by RELAT_1: 61;

      now

        let s1;

        assume that

         A8: ( rng s1) c= ( dom ((f ^ ) | X)) and

         A9: s1 is convergent & ( lim s1) = g;

        ( rng s1) c= (( dom (f ^ )) /\ X) by A8, RELAT_1: 61;

        then

         A10: ( rng s1) c= ( dom (f | X)) by A3, RELAT_1: 61;

        then

         A11: ((f | X) /* s1) is convergent by A6, A9;

        now

          let n be Element of NAT ;

          

           A12: (s1 . n) in ( rng s1) by VALUED_0: 28;

          ( rng s1) c= (( dom f) /\ X) & (( dom f) /\ X) c= ( dom f) by A3, A8, RELAT_1: 61, XBOOLE_1: 17;

          then

           A13: ( rng s1) c= ( dom f);

           A14:

          now

            assume (f /. (s1 . n)) = 0c ;

            then (f /. (s1 . n)) in { 0c } by TARSKI:def 1;

            hence contradiction by A2, A13, A12, PARTFUN2: 26;

          end;

          (((f | X) /* s1) . n) = ((f | X) /. (s1 . n)) by A10, FUNCT_2: 109

          .= (f /. (s1 . n)) by A10, A12, PARTFUN2: 15;

          hence (((f | X) /* s1) . n) <> 0c by A14;

        end;

        then

         A15: ((f | X) /* s1) is non-zero by COMSEQ_1: 4;

        g in (( dom f) /\ X) by A3, A4, A5, XBOOLE_0:def 4;

        then

         A16: g in ( dom (f | X)) by RELAT_1: 61;

        then

         A17: ((f | X) /. g) = (f /. g) by PARTFUN2: 15;

        now

          let n be Element of NAT ;

          

           A18: (s1 . n) in ( rng s1) by VALUED_0: 28;

          then (s1 . n) in ( dom ((f ^ ) | X)) by A8;

          then (s1 . n) in (( dom (f ^ )) /\ X) by RELAT_1: 61;

          then

           A19: (s1 . n) in ( dom (f ^ )) by XBOOLE_0:def 4;

          

          thus ((((f ^ ) | X) /* s1) . n) = (((f ^ ) | X) /. (s1 . n)) by A8, FUNCT_2: 109

          .= ((f ^ ) /. (s1 . n)) by A8, A18, PARTFUN2: 15

          .= ((f /. (s1 . n)) " ) by A19, CFUNCT_1:def 2

          .= (((f | X) /. (s1 . n)) " ) by A10, A18, PARTFUN2: 15

          .= ((((f | X) /* s1) . n) " ) by A10, FUNCT_2: 109

          .= ((((f | X) /* s1) " ) . n) by VALUED_1: 10;

        end;

        then

         A20: (((f ^ ) | X) /* s1) = (((f | X) /* s1) " ) by FUNCT_2: 63;

        reconsider gg = g as Element of COMPLEX by XCMPLX_0:def 2;

         A21:

        now

          assume (f /. g) = 0c ;

          then (f /. gg) in { 0c } by TARSKI:def 1;

          hence contradiction by A2, A3, A4, A5, PARTFUN2: 26;

        end;

        then ( lim ((f | X) /* s1)) <> 0c by A6, A9, A10, A17;

        hence (((f ^ ) | X) /* s1) is convergent by A11, A15, A20, COMSEQ_2: 34;

        ((f | X) /. g) = ( lim ((f | X) /* s1)) by A6, A9, A10;

        

        hence ( lim (((f ^ ) | X) /* s1)) = (((f | X) /. g) " ) by A11, A17, A21, A15, A20, COMSEQ_2: 35

        .= ((f /. g) " ) by A16, PARTFUN2: 15

        .= ((f ^ ) /. gg) by A4, A5, CFUNCT_1:def 2

        .= (((f ^ ) | X) /. g) by A7, PARTFUN2: 15;

      end;

      hence thesis by A7;

    end;

    theorem :: CFCONT_1:48

    f is_continuous_on X & ((f | X) " { 0 }) = {} implies (f ^ ) is_continuous_on X

    proof

      assume that

       A1: f is_continuous_on X and

       A2: ((f | X) " { 0 }) = {} ;

      (f | X) is_continuous_on X by A1, Th40;

      then ((f | X) ^ ) is_continuous_on X by A2, Th47;

      then ((f ^ ) | X) is_continuous_on X by CFUNCT_1: 54;

      hence thesis by Th40;

    end;

    theorem :: CFCONT_1:49

    f1 is_continuous_on X & (f1 " { 0 }) = {} & f2 is_continuous_on X implies (f2 / f1) is_continuous_on X

    proof

      assume that

       A1: f1 is_continuous_on X & (f1 " { 0 }) = {} and

       A2: f2 is_continuous_on X;

      (f1 ^ ) is_continuous_on X by A1, Th47;

      then (f2 (#) (f1 ^ )) is_continuous_on X by A2, Th43;

      hence thesis by CFUNCT_1: 39;

    end;

    theorem :: CFCONT_1:50

    f is total & (for x1, x2 holds (f /. (x1 + x2)) = ((f /. x1) + (f /. x2))) & (ex x0 st f is_continuous_in x0) implies f is_continuous_on COMPLEX

    proof

      assume that

       A1: f is total and

       A2: for x1, x2 holds (f /. (x1 + x2)) = ((f /. x1) + (f /. x2)) and

       A3: ex x0 st f is_continuous_in x0;

      

       A4: ( dom f) = COMPLEX by A1, PARTFUN1:def 2;

      consider x0 such that

       A5: f is_continuous_in x0 by A3;

      

       A6: ((f /. x0) + 0c ) = (f /. (x0 + 0c ))

      .= ((f /. x0) + (f /. 0c )) by A2;

       A7:

      now

        let x1;

         0c = (f /. (x1 + ( - x1))) by A6

        .= ((f /. x1) + (f /. ( - x1))) by A2;

        hence ( - (f /. x1)) = (f /. ( - x1));

      end;

       A8:

      now

        let x1, x2;

        

        thus (f /. (x1 - x2)) = (f /. (x1 + ( - x2)))

        .= ((f /. x1) + (f /. ( - x2))) by A2

        .= ((f /. x1) + ( - (f /. x2))) by A7

        .= ((f /. x1) - (f /. x2));

      end;

      now

        let x1, r;

        assume that x1 in COMPLEX and

         A9: r > 0 ;

        set y = (x1 - x0);

        consider s such that

         A10: 0 < s and

         A11: for x1 st x1 in ( dom f) & |.(x1 - x0).| < s holds |.((f /. x1) - (f /. x0)).| < r by A5, A9, Th32;

        take s;

        thus s > 0 by A10;

        let x2 such that x2 in COMPLEX and

         A12: |.(x2 - x1).| < s;

        

         A13: |.((x2 - y) - x0).| = |.(x2 - x1).|;

        

         A14: (x2 - y) in ( dom f) by A4, XCMPLX_0:def 2;

        ((x1 - x0) + x0) = x1;

        

        then |.((f /. x2) - (f /. x1)).| = |.((f /. x2) - ((f /. y) + (f /. x0))).| by A2

        .= |.(((f /. x2) - (f /. y)) - (f /. x0)).|

        .= |.((f /. (x2 - y)) - (f /. x0)).| by A8;

        hence |.((f /. x2) - (f /. x1)).| < r by A11, A12, A13, A14;

      end;

      hence thesis by A4, Th39;

    end;

    definition

      let X;

      :: CFCONT_1:def3

      attr X is compact means for s1 st ( rng s1) c= X holds ex s2 st s2 is subsequence of s1 & s2 is convergent & ( lim s2) in X;

    end

    theorem :: CFCONT_1:51

    

     Th51: for f st ( dom f) is compact & f is_continuous_on ( dom f) holds ( rng f) is compact

    proof

      let f;

      assume that

       A1: ( dom f) is compact and

       A2: f is_continuous_on ( dom f);

      now

        let s1 such that

         A3: ( rng s1) c= ( rng f);

        defpred P[ object, object] means $2 in ( dom f) & (f /. $2) = (s1 . $1);

        

         A4: for n holds ex g st P[n, g]

        proof

          let n;

          (s1 . n) in ( rng s1) by VALUED_0: 28;

          then

          consider g be Element of COMPLEX such that

           A5: g in ( dom f) & (s1 . n) = (f . g) by A3, PARTFUN1: 3;

          take g;

          thus thesis by A5, PARTFUN1:def 6;

        end;

        consider q1 such that

         A6: for n holds P[n, (q1 . n)] from CompSeqChoice( A4);

        now

          let x be object;

          assume x in ( rng q1);

          then ex n be Element of NAT st x = (q1 . n) by FUNCT_2: 113;

          hence x in ( dom f) by A6;

        end;

        then

         A7: ( rng q1) c= ( dom f);

        then

        consider s2 such that

         A8: s2 is subsequence of q1 and

         A9: s2 is convergent and

         A10: ( lim s2) in ( dom f) by A1;

        take q2 = (f /* s2);

        ( rng s2) c= ( rng q1) by A8, VALUED_0: 21;

        then

         A11: ( rng s2) c= ( dom f) by A7;

        now

          let n be Element of NAT ;

          (f /. (q1 . n)) = (s1 . n) by A6;

          hence ((f /* q1) . n) = (s1 . n) by A7, FUNCT_2: 109;

        end;

        then

         A12: (f /* q1) = s1 by FUNCT_2: 63;

        (f | ( dom f)) is_continuous_in ( lim s2) by A2, A10;

        then

         A13: f is_continuous_in ( lim s2) by RELAT_1: 68;

        then (f /. ( lim s2)) = ( lim (f /* s2)) by A9, A11;

        then (f . ( lim s2)) = ( lim (f /* s2)) by A10, PARTFUN1:def 6;

        hence q2 is subsequence of s1 & q2 is convergent & ( lim q2) in ( rng f) by A7, A12, A8, A9, A13, A11, FUNCT_1:def 3, VALUED_0: 22;

      end;

      hence thesis;

    end;

    theorem :: CFCONT_1:52

    Y c= ( dom f) & Y is compact & f is_continuous_on Y implies (f .: Y) is compact

    proof

      assume that

       A1: Y c= ( dom f) and

       A2: Y is compact and

       A3: f is_continuous_on Y;

      

       A4: ( dom (f | Y)) = (( dom f) /\ Y) by RELAT_1: 61

      .= Y by A1, XBOOLE_1: 28;

      (f | Y) is_continuous_on Y

      proof

        thus Y c= ( dom (f | Y)) by A4;

        let g;

        assume g in Y;

        then (f | Y) is_continuous_in g by A3;

        hence thesis by RELAT_1: 72;

      end;

      then ( rng (f | Y)) is compact by A2, A4, Th51;

      hence thesis by RELAT_1: 115;

    end;