cfdiff_1.miz



    begin

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

    reserve X,y for set;

    reserve p for Real;

    reserve r for Real;

    reserve a,a1,a2,b,b1,b2,x,x0,z,z0 for Complex;

    reserve s1,s3,seq,seq1 for Complex_Sequence;

    reserve Y for Subset of COMPLEX ;

    reserve f,f1,f2 for PartFunc of COMPLEX , COMPLEX ;

    reserve Nseq for increasing sequence of NAT ;

    definition

      let x be Real;

      let IT be Complex_Sequence;

      :: CFDIFF_1:def1

      attr IT is x -convergent means

      : Def1: IT is convergent & ( lim IT) = x;

    end

    theorem :: CFDIFF_1:1

    for rs be Real_Sequence, cs be Complex_Sequence st rs = cs & rs is convergent holds cs is convergent;

    definition

      let r be Real;

      :: CFDIFF_1:def2

      func InvShift (r) -> Complex_Sequence means

      : Def2: for n holds (it . n) = (1 / (n + r));

      existence

      proof

        deffunc F( Real) = (1 / ($1 + r));

        ex seq st for n holds (seq . n) = F(n) from COMSEQ_1:sch 1;

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Complex_Sequence such that

         A1: for n holds (f . n) = (1 / (n + r)) and

         A2: for n holds (g . n) = (1 / (n + r));

        let n be Element of NAT ;

        

        thus (f . n) = (1 / (n + r)) by A1

        .= (g . n) by A2;

      end;

    end

    theorem :: CFDIFF_1:2

    

     Th2: 0 < r implies ( InvShift r) is convergent

    proof

      assume

       A1: 0 < r;

      set seq = ( InvShift r);

      take g = 0c ;

      let p;

      assume

       A2: 0 < p;

      consider k1 such that

       A3: (p " ) < k1 by SEQ_4: 3;

      take n = k1;

      let m;

      assume n <= m;

      then (n + r) <= (m + r) by XREAL_1: 6;

      then

       A4: (1 / (m + r)) <= (1 / (n + r)) by A1, XREAL_1: 118;

      

       A5: (seq . m) = (1 / (m + r)) by Def2;

      ((p " ) + 0 ) < (k1 + r) by A1, A3, XREAL_1: 8;

      then (1 / (k1 + r)) < (1 / (p " )) by A2, XREAL_1: 76;

      then (1 / (m + r)) < p by A4, XXREAL_0: 2;

      hence |.((seq . m) - g).| < p by A1, A5, ABSVALUE:def 1;

    end;

    registration

      let r be positive Real;

      cluster ( InvShift r) -> convergent;

      coherence by Th2;

    end

    theorem :: CFDIFF_1:3

    

     Th3: 0 < r implies ( lim ( InvShift r)) = 0

    proof

      set seq = ( InvShift r);

      assume

       A1: 0 < r;

      now

        let p;

        assume

         A2: 0 < p;

        consider k1 such that

         A3: (p " ) < k1 by SEQ_4: 3;

        take n = k1;

        let m;

        assume n <= m;

        then (n + r) <= (m + r) by XREAL_1: 6;

        then

         A4: (1 / (m + r)) <= (1 / (n + r)) by A1, XREAL_1: 118;

        

         A5: (seq . m) = (1 / (m + r)) by Def2;

        ((p " ) + 0 ) < (k1 + r) by A1, A3, XREAL_1: 8;

        then (1 / (k1 + r)) < (1 / (p " )) by A2, XREAL_1: 76;

        then (1 / (m + r)) < p by A4, XXREAL_0: 2;

        hence |.((seq . m) - 0c ).| < p by A1, A5, ABSVALUE:def 1;

      end;

      hence thesis by A1, COMSEQ_2:def 6;

    end;

    registration

      let r be positive Real;

      cluster ( InvShift r) -> non-zero 0 -convergent;

      coherence

      proof

        set s = ( InvShift r);

        now

          let n be Element of NAT ;

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

          hence (s . n) <> 0c by Def2;

        end;

        hence s is non-zero by COMSEQ_1: 4;

        ( lim s) = 0 by Th3;

        hence thesis;

      end;

    end

    registration

      cluster 0 -convergent non-zero for Complex_Sequence;

      existence

      proof

        take ( InvShift 1);

        thus thesis;

      end;

    end

    registration

      cluster 0 -convergent non-zero -> convergent for Complex_Sequence;

      coherence ;

    end

    registration

      cluster constant for Complex_Sequence;

      existence

      proof

        reconsider cs = ( NAT --> 0c ) as Complex_Sequence;

        take cs;

        thus thesis;

      end;

    end

    theorem :: CFDIFF_1:4

    seq is constant iff for n, m holds (seq . n) = (seq . m)

    proof

      thus seq is constant implies for n, m holds (seq . n) = (seq . m) by VALUED_0: 23;

      assume that

       A1: for n, m holds (seq . n) = (seq . m) and

       A2: seq is non constant;

      now

        let n be Nat;

        consider n1 be Nat such that

         A3: (seq . n1) <> (seq . n) by A2, VALUED_0:def 18;

        thus contradiction by A1, A3;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:5

    for n holds ((seq * Nseq) . n) = (seq . (Nseq . n))

    proof

      let n;

      

       A1: n in NAT by ORDINAL1:def 12;

      ( dom (seq * Nseq)) = NAT by FUNCT_2:def 1;

      hence thesis by FUNCT_1: 12, A1;

    end;

    reserve h for 0 -convergent non-zero Complex_Sequence;

    reserve c for constant Complex_Sequence;

    definition

      let IT be PartFunc of COMPLEX , COMPLEX ;

      :: CFDIFF_1:def3

      attr IT is RestFunc-like means

      : Def3: for h holds ((h " ) (#) (IT /* h)) is convergent & ( lim ((h " ) (#) (IT /* h))) = 0 ;

    end

    registration

      cluster total RestFunc-like for PartFunc of COMPLEX , COMPLEX ;

      existence

      proof

        reconsider cf = ( COMPLEX --> 0c ) as Function of COMPLEX , COMPLEX ;

        take f = cf;

        thus f is total;

        let h;

        now

          let n be Nat;

          

           A1: n in NAT & ( rng h) c= ( dom f) by ORDINAL1:def 12;

          

          thus (((h " ) (#) (f /* h)) . n) = (((h " ) . n) * ((f /* h) . n)) by VALUED_1: 5

          .= (((h " ) . n) * (f /. (h . n))) by A1, FUNCT_2: 108

          .= (((h " ) . n) * 0c )

          .= 0c ;

        end;

        then ((h " ) (#) (f /* h)) is constant & (((h " ) (#) (f /* h)) . 0 ) = 0c by VALUED_0:def 18;

        hence ((h " ) (#) (f /* h)) is convergent & ( lim ((h " ) (#) (f /* h))) = 0c by CFCONT_1: 26, CFCONT_1: 27;

      end;

    end

    definition

      mode C_RestFunc is total RestFunc-like PartFunc of COMPLEX , COMPLEX ;

    end

    definition

      let IT be PartFunc of COMPLEX , COMPLEX ;

      :: CFDIFF_1:def4

      attr IT is linear means

      : Def4: ex a st for z holds (IT /. z) = (a * z);

    end

    registration

      cluster total linear for PartFunc of COMPLEX , COMPLEX ;

      existence

      proof

        deffunc F( Complex) = ( In (( 1r * $1), COMPLEX ));

        defpred P[ set] means $1 in COMPLEX ;

        consider f such that

         A1: (for a be Element of COMPLEX holds a in ( dom f) iff P[a]) & for a be Element of COMPLEX st a in ( dom f) holds (f . a) = F(a) from SEQ_1:sch 3;

        take f;

        for y be object holds y in COMPLEX implies y in ( dom f) by A1;

        then COMPLEX c= ( dom f);

        then

         A2: ( dom f) = COMPLEX ;

        hence f is total by PARTFUN1:def 2;

        take 1r ;

        let z;

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

        (f /. z) = (f . z) by A2, PARTFUN1:def 6

        .= F(z) by A1;

        hence thesis;

      end;

    end

    definition

      mode C_LinearFunc is total linear PartFunc of COMPLEX , COMPLEX ;

    end

    reserve R,R1,R2 for C_RestFunc;

    reserve L,L1,L2 for C_LinearFunc;

    registration

      let L1, L2;

      cluster (L1 + L2) -> total linear;

      coherence

      proof

        consider a2 such that

         A1: for z holds (L2 /. z) = (a2 * z) by Def4;

        consider a1 such that

         A2: for z holds (L1 /. z) = (a1 * z) by Def4;

        now

          let z;

          z in COMPLEX by XCMPLX_0:def 2;

          

          hence ((L1 + L2) /. z) = ((L1 /. z) + (L2 /. z)) by CFUNCT_1: 64

          .= ((a1 * z) + (L2 /. z)) by A2

          .= ((a1 * z) + (a2 * z)) by A1

          .= ((a1 + a2) * z);

        end;

        hence thesis;

      end;

      cluster (L1 - L2) -> total linear;

      coherence

      proof

        consider a2 such that

         A3: for z holds (L2 /. z) = (a2 * z) by Def4;

        consider a1 such that

         A4: for z holds (L1 /. z) = (a1 * z) by Def4;

        now

          let z;

          z in COMPLEX by XCMPLX_0:def 2;

          

          hence ((L1 - L2) /. z) = ((L1 /. z) - (L2 /. z)) by CFUNCT_1: 64

          .= ((a1 * z) - (L2 /. z)) by A4

          .= ((a1 * z) - (a2 * z)) by A3

          .= ((a1 - a2) * z);

        end;

        hence thesis;

      end;

    end

    registration

      let a, L;

      cluster (a (#) L) -> total linear;

      coherence

      proof

        consider b such that

         A1: for z holds (L /. z) = (b * z) by Def4;

        now

          let z;

          z in COMPLEX by XCMPLX_0:def 2;

          

          hence ((a (#) L) /. z) = (a * (L /. z)) by CFUNCT_1: 65

          .= (a * (b * z)) by A1

          .= ((a * b) * z);

        end;

        hence thesis;

      end;

    end

    registration

      let R1, R2;

      cluster (R1 + R2) -> total RestFunc-like;

      coherence

      proof

        now

          let h;

          

           A1: ((h " ) (#) ((R1 + R2) /* h)) = ((h " ) (#) ((R1 /* h) + (R2 /* h))) by CFCONT_1: 14

          .= (((h " ) (#) (R1 /* h)) + ((h " ) (#) (R2 /* h))) by COMSEQ_1: 10;

          

           A2: ((h " ) (#) (R1 /* h)) is convergent & ((h " ) (#) (R2 /* h)) is convergent by Def3;

          hence ((h " ) (#) ((R1 + R2) /* h)) is convergent by A1;

          

           A3: ( lim ((h " ) (#) (R1 /* h))) = 0 by Def3;

          

          thus ( lim ((h " ) (#) ((R1 + R2) /* h))) = (( lim ((h " ) (#) (R1 /* h))) + ( lim ((h " ) (#) (R2 /* h)))) by A2, A1, COMSEQ_2: 14

          .= 0 by A3, Def3;

        end;

        hence thesis;

      end;

      cluster (R1 - R2) -> total RestFunc-like;

      coherence

      proof

        now

          let h;

          

           A4: ((h " ) (#) ((R1 - R2) /* h)) = ((h " ) (#) ((R1 /* h) - (R2 /* h))) by CFCONT_1: 14

          .= (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R2 /* h))) by COMSEQ_1: 15;

          

           A5: ((h " ) (#) (R1 /* h)) is convergent & ((h " ) (#) (R2 /* h)) is convergent by Def3;

          hence ((h " ) (#) ((R1 - R2) /* h)) is convergent by A4;

          ( lim ((h " ) (#) (R1 /* h))) = 0c & ( lim ((h " ) (#) (R2 /* h))) = 0c by Def3;

          

          hence ( lim ((h " ) (#) ((R1 - R2) /* h))) = ( 0c - 0c ) by A5, A4, COMSEQ_2: 26

          .= 0c ;

        end;

        hence thesis;

      end;

      cluster (R1 (#) R2) -> total RestFunc-like;

      coherence

      proof

        now

          let h;

          seq is non-zero implies (seq " ) is non-zero

          proof

            assume that

             A6: seq is non-zero and

             A7: not (seq " ) is non-zero;

            consider n1 be Element of NAT such that

             A8: ((seq " ) . n1) = 0c by A7, COMSEQ_1: 4;

            ((seq . n1) " ) = ((seq " ) . n1) by VALUED_1: 10;

            hence contradiction by A6, A8, COMSEQ_1: 4, XCMPLX_1: 202;

          end;

          then

           A9: (h " ) is non-zero;

          

           A10: ((h " ) (#) ((R1 (#) R2) /* h)) = (((R1 /* h) (#) (R2 /* h)) /" h) by CFCONT_1: 14

          .= ((((R1 /* h) (#) (R2 /* h)) (#) (h " )) /" (h (#) (h " ))) by A9, COMSEQ_1: 37

          .= ((((R1 /* h) (#) (R2 /* h)) (#) (h " )) (#) (((h " ) " ) (#) (h " ))) by COMSEQ_1: 30

          .= ((h (#) (h " )) (#) ((R1 /* h) (#) ((h " ) (#) (R2 /* h)))) by COMSEQ_1: 8

          .= (((h (#) (h " )) (#) (R1 /* h)) (#) ((h " ) (#) (R2 /* h))) by COMSEQ_1: 8

          .= ((h (#) ((h " ) (#) (R1 /* h))) (#) ((h " ) (#) (R2 /* h))) by COMSEQ_1: 8;

          

           A11: ((h " ) (#) (R1 /* h)) is convergent by Def3;

          then

           A12: (h (#) ((h " ) (#) (R1 /* h))) is convergent;

          ( lim ((h " ) (#) (R1 /* h))) = 0c & ( lim h) = 0c by Def1, Def3;

          

          then

           A13: ( lim (h (#) ((h " ) (#) (R1 /* h)))) = ( 0 * 0 ) by A11, COMSEQ_2: 30

          .= 0c ;

          

           A14: ((h " ) (#) (R2 /* h)) is convergent by Def3;

          hence ((h " ) (#) ((R1 (#) R2) /* h)) is convergent by A12, A10;

          ( lim ((h " ) (#) (R2 /* h))) = 0c by Def3;

          

          hence ( lim ((h " ) (#) ((R1 (#) R2) /* h))) = ( 0c * 0c ) by A14, A12, A13, A10, COMSEQ_2: 30

          .= 0c ;

        end;

        hence thesis;

      end;

    end

    registration

      let a, R;

      cluster (a (#) R) -> total RestFunc-like;

      coherence

      proof

        now

          let h;

          

           A1: ((h " ) (#) ((a (#) R) /* h)) = ((h " ) (#) (a (#) (R /* h))) by CFCONT_1: 15

          .= (a (#) ((h " ) (#) (R /* h))) by COMSEQ_1: 13;

          

           A2: ((h " ) (#) (R /* h)) is convergent by Def3;

          hence ((h " ) (#) ((a (#) R) /* h)) is convergent by A1;

          ( lim ((h " ) (#) (R /* h))) = 0c by Def3;

          

          hence ( lim ((h " ) (#) ((a (#) R) /* h))) = (a * 0c ) by A2, A1, COMSEQ_2: 18

          .= 0c ;

        end;

        hence thesis;

      end;

    end

    registration

      let L1, L2;

      cluster (L1 (#) L2) -> total RestFunc-like;

      coherence

      proof

        reconsider LL = (L1 (#) L2) as PartFunc of COMPLEX , COMPLEX ;

        LL is RestFunc-like

        proof

          let h;

          consider b1 such that

           A1: for z holds (L1 /. z) = (b1 * z) by Def4;

          consider b2 such that

           A2: for z holds (L2 /. z) = (b2 * z) by Def4;

           A3:

          now

            let n be Element of NAT ;

            

             A4: (h . n) <> 0c by COMSEQ_1: 4;

            

            thus (((h " ) (#) ((L1 (#) L2) /* h)) . n) = (((h " ) . n) * (((L1 (#) L2) /* h) . n)) by VALUED_1: 5

            .= (((h " ) . n) * ((L1 (#) L2) /. (h . n))) by FUNCT_2: 115

            .= (((h " ) . n) * ((L1 /. (h . n)) * (L2 /. (h . n)))) by CFUNCT_1: 64

            .= ((((h " ) . n) * (L1 /. (h . n))) * (L2 /. (h . n)))

            .= ((((h . n) " ) * (L1 /. (h . n))) * (L2 /. (h . n))) by VALUED_1: 10

            .= ((((h . n) " ) * ((h . n) * b1)) * (L2 /. (h . n))) by A1

            .= (((((h . n) " ) * (h . n)) * b1) * (L2 /. (h . n)))

            .= (( 1r * b1) * (L2 /. (h . n))) by A4, XCMPLX_0:def 7

            .= (b1 * (b2 * (h . n))) by A2

            .= ((b1 * b2) * (h . n))

            .= (((b1 * b2) (#) h) . n) by VALUED_1: 6;

          end;

          then

           A5: ((h " ) (#) ((L1 (#) L2) /* h)) = ((b1 * b2) (#) h);

          thus ((h " ) (#) (LL /* h)) is convergent by A3, FUNCT_2: 63;

          ( lim h) = 0c by Def1;

          

          hence ( lim ((h " ) (#) (LL /* h))) = ((b1 * b2) * 0c ) by A5, COMSEQ_2: 18

          .= 0c ;

        end;

        hence thesis;

      end;

    end

    registration

      let R, L;

      cluster (R (#) L) -> total RestFunc-like;

      coherence

      proof

        consider b1 such that

         A1: for z holds (L /. z) = (b1 * z) by Def4;

        now

          let h;

          

           A2: ((h " ) (#) ((R (#) L) /* h)) = ((h " ) (#) ((R /* h) (#) (L /* h))) by CFCONT_1: 14

          .= (((h " ) (#) (R /* h)) (#) (L /* h)) by COMSEQ_1: 8;

          now

            let n be Element of NAT ;

            

            thus ((L /* h) . n) = (L /. (h . n)) by FUNCT_2: 115

            .= (b1 * (h . n)) by A1

            .= ((b1 (#) h) . n) by VALUED_1: 6;

          end;

          then

           A3: (L /* h) = (b1 (#) h);

          ( lim h) = 0c by Def1;

          

          then

           A4: ( lim (L /* h)) = (b1 * 0c ) by A3, COMSEQ_2: 18

          .= 0c ;

          

           A5: ((h " ) (#) (R /* h)) is convergent by Def3;

          hence ((h " ) (#) ((R (#) L) /* h)) is convergent by A2, A3;

          ( lim ((h " ) (#) (R /* h))) = 0c by Def3;

          

          hence ( lim ((h " ) (#) ((R (#) L) /* h))) = ( 0c * 0c ) by A2, A3, A4, A5, COMSEQ_2: 30

          .= 0c ;

        end;

        hence thesis;

      end;

      cluster (L (#) R) -> total RestFunc-like;

      coherence ;

    end

    definition

      let z0 be Complex;

      :: CFDIFF_1:def5

      mode Neighbourhood of z0 -> Subset of COMPLEX means

      : Def5: ex g be Real st 0 < g & { y where y be Complex : |.(y - z0).| < g } c= it ;

      existence

      proof

        set N = { y where y be Complex : |.(y - z0).| < 1 };

        take N;

        N c= COMPLEX

        proof

          let z be object;

          assume z in { y where y be Complex : |.(y - z0).| < 1 };

          then ex y be Complex st z = y & |.(y - z0).| < 1;

          hence thesis by XCMPLX_0:def 2;

        end;

        hence thesis;

      end;

    end

    theorem :: CFDIFF_1:6

    

     Th6: for g be Real st 0 < g holds { y where y be Complex : |.(y - z0).| < g } is Neighbourhood of z0

    proof

      let g be Real such that

       A1: g > 0 ;

      set N = { y where y be Complex : |.(y - z0).| < g };

      

       A2: N c= COMPLEX

      proof

        let z be object;

        assume z in { y where y be Complex : |.(y - z0).| < g };

        then ex y be Complex st z = y & |.(y - z0).| < g;

        hence thesis by XCMPLX_0:def 2;

      end;

      thus thesis by A1, A2, Def5;

    end;

    theorem :: CFDIFF_1:7

    

     Th7: for N be Neighbourhood of z0 holds z0 in N

    proof

      let N be Neighbourhood of z0;

      consider g be Real such that

       A1: 0 < g and

       A2: { z where z be Complex : |.(z - z0).| < g } c= N by Def5;

       |.(z0 - z0).| = 0 by COMPLEX1: 44;

      then z0 in { z where z be Complex : |.(z - z0).| < g } by A1;

      hence thesis by A2;

    end;

    

     Lm1: for z0 be Complex holds for N1,N2 be Neighbourhood of z0 holds ex N be Neighbourhood of z0 st N c= N1 & N c= N2

    proof

      let z0 be Complex;

      let N1,N2 be Neighbourhood of z0;

      consider a1 be Real such that

       A1: 0 < a1 and

       A2: { y where y be Complex : |.(y - z0).| < a1 } c= N1 by Def5;

      consider a2 be Real such that

       A3: 0 < a2 and

       A4: { y where y be Complex : |.(y - z0).| < a2 } c= N2 by Def5;

      set g = ( min (a1,a2));

      take IT = { y where y be Complex : |.(y - z0).| < g };

      

       A5: g <= a2 by XXREAL_0: 17;

      

       A6: { y where y be Complex : |.(y - z0).| < g } c= { y where y be Complex : |.(y - z0).| < a2 }

      proof

        let z be object;

        assume z in { y where y be Complex : |.(y - z0).| < g };

        then

        consider y be Complex such that

         A7: z = y and

         A8: |.(y - z0).| < g;

         |.(y - z0).| < a2 by A5, A8, XXREAL_0: 2;

        hence thesis by A7;

      end;

      

       A9: g <= a1 by XXREAL_0: 17;

      

       A10: { y where y be Complex : |.(y - z0).| < g } c= { y where y be Complex : |.(y - z0).| < a1 }

      proof

        let z be object;

        assume z in { y where y be Complex : |.(y - z0).| < g };

        then

        consider y be Complex such that

         A11: z = y and

         A12: |.(y - z0).| < g;

         |.(y - z0).| < a1 by A9, A12, XXREAL_0: 2;

        hence thesis by A11;

      end;

       0 < g by A1, A3, XXREAL_0: 15;

      hence thesis by A2, A4, A10, A6, Th6;

    end;

    definition

      let f;

      let z0 be Complex;

      :: CFDIFF_1:def6

      pred f is_differentiable_in z0 means ex N be Neighbourhood of z0 st N c= ( dom f) & ex L, R st for z st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0)));

    end

    definition

      let f;

      let z0 be Complex;

      assume

       A1: f is_differentiable_in z0;

      :: CFDIFF_1:def7

      func diff (f,z0) -> Element of COMPLEX means

      : Def7: ex N be Neighbourhood of z0 st N c= ( dom f) & ex L, R st it = (L /. 1r ) & for z st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0)));

      existence

      proof

        consider N be Neighbourhood of z0 such that

         A2: N c= ( dom f) and

         A3: ex L, R st for z st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) by A1;

        consider L, R such that

         A4: for z st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) by A3;

        consider a be Complex such that

         A5: for d be Complex holds (L /. d) = (a * d) by Def4;

        take a;

        (L /. 1r ) = (a * 1r ) by A5

        .= a;

        hence thesis by A2, A4;

      end;

      uniqueness

      proof

        set s0 = ( InvShift 2);

        let a,b be Element of COMPLEX ;

        assume that

         A6: ex N be Neighbourhood of z0 st N c= ( dom f) & ex L, R st a = (L /. 1r ) & for z st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) and

         A7: ex N be Neighbourhood of z0 st N c= ( dom f) & ex L, R st b = (L /. 1r ) & for z st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0)));

        consider N be Neighbourhood of z0 such that N c= ( dom f) and

         A8: ex L, R st a = (L /. 1r ) & for z st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) by A6;

        consider L, R such that

         A9: a = (L /. 1r ) and

         A10: for z st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) by A8;

        consider a1 such that

         A11: for b holds (L /. b) = (a1 * b) by Def4;

        consider N1 be Neighbourhood of z0 such that N1 c= ( dom f) and

         A12: ex L, R st b = (L /. 1r ) & for z st z in N1 holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) by A7;

        consider L1, R1 such that

         A13: b = (L1 /. 1r ) and

         A14: for z st z in N1 holds ((f /. z) - (f /. z0)) = ((L1 /. (z - z0)) + (R1 /. (z - z0))) by A12;

        consider b1 such that

         A15: for b holds (L1 /. b) = (b1 * b) by Def4;

        reconsider s0 as Complex_Sequence;

        consider N0 be Neighbourhood of z0 such that

         A16: N0 c= N & N0 c= N1 by Lm1;

        consider g be Real such that

         A17: 0 < g and

         A18: { y where y be Complex : |.(y - z0).| < g } c= N0 by Def5;

        set s1 = (g (#) s0);

         A19:

        now

          let n;

          

          thus (s1 . n) = (g * (s0 . n)) by VALUED_1: 6

          .= (g * (1 / (n + 2))) by Def2

          .= (g / (n + 2));

        end;

        now

          let n be Element of NAT ;

          (s1 . n) = (g / (n + 2)) by A19;

          hence 0 <> (s1 . n) by A17;

        end;

        then

         A20: s1 is non-zero by COMSEQ_1: 4;

        ( lim s0) = 0 by Th3;

        then ( lim s1) = (g * 0 ) by COMSEQ_2: 18;

        then

        reconsider h = s1 as 0 -convergent non-zero Complex_Sequence by A20, Def1;

        

         A21: for n holds ex x be Complex st x in N & x in N1 & (h . n) = (x - z0)

        proof

          let n;

          reconsider g0 = (g / (n + 2)) as Complex;

          take x = (z0 + g0);

          ( 0 + 1) < ((n + 1) + 1) by XREAL_1: 6;

          then

           A22: (g / (n + 2)) < (g / 1) by A17, XREAL_1: 76;

           |.((z0 + g0) - z0).| = (g / (n + 2)) by A17, ABSVALUE:def 1;

          then x in { y where y be Complex : |.(y - z0).| < g } by A22;

          then x in N0 by A18;

          hence thesis by A16, A19;

        end;

        

         A23: a = (a1 * 1r ) by A9, A11;

         A24:

        now

          let z be Complex;

          assume that

           A25: z in N and

           A26: z in N1;

          reconsider t0 = z0, t = z as Element of COMPLEX by XCMPLX_0:def 2;

          ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) by A10, A25;

          then ((L /. (z - z0)) + (R /. (z - z0))) = ((L1 /. (z - z0)) + (R1 /. (z - z0))) by A14, A26;

          then ((a1 * (t - t0)) + (R /. (t - t0))) = ((L1 /. (t - t0)) + (R1 /. (t - t0))) by A11;

          then (((a1 * 1r ) * (z - z0)) + (R /. (z - z0))) = (((b1 * 1r ) * (z - z0)) + (R1 /. (z - z0))) by A15;

          hence ((a * (z - z0)) + (R /. (z - z0))) = ((b * (z - z0)) + (R1 /. (z - z0))) by A13, A15, A23;

        end;

        

         A27: (a - b) in COMPLEX by XCMPLX_0:def 2;

        now

          ( dom R1) = COMPLEX by PARTFUN1:def 2;

          then

           A28: ( rng h) c= ( dom R1);

          ( dom R) = COMPLEX by PARTFUN1:def 2;

          then

           A29: ( rng h) c= ( dom R);

          let n be Nat;

          

           A30: n in NAT by ORDINAL1:def 12;

          then

           A31: (h . n) <> 0c by COMSEQ_1: 4;

          ex x be Complex st x in N & x in N1 & (h . n) = (x - z0) by A21;

          then ((a * (h . n)) + (R /. (h . n))) = ((b * (h . n)) + (R1 /. (h . n))) by A24;

          then

           A32: (((a * (h . n)) / (h . n)) + ((R /. (h . n)) / (h . n))) = (((b * (h . n)) + (R1 /. (h . n))) / (h . n)) by XCMPLX_1: 62;

          

           A33: ((b * (h . n)) / (h . n)) = (b * ((h . n) / (h . n)))

          .= (b * 1) by A31, XCMPLX_1: 60

          .= b;

          

           A34: ((R1 /. (h . n)) / (h . n)) = ((R1 /. (h . n)) * ((h " ) . n)) by VALUED_1: 10

          .= (((R1 /* h) . n) * ((h " ) . n)) by A30, A28, FUNCT_2: 108

          .= (((h " ) (#) (R1 /* h)) . n) by VALUED_1: 5;

          

           A35: ((a * (h . n)) / (h . n)) = (a * ((h . n) / (h . n)))

          .= (a * 1) by A31, XCMPLX_1: 60

          .= a;

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

          .= (((R /* h) . n) * ((h " ) . n)) by A30, A29, FUNCT_2: 109

          .= (((h " ) (#) (R /* h)) . n) by VALUED_1: 5;

          

          hence (a - b) = ((((h " ) (#) (R1 /* h)) . n) + ( - (((h " ) (#) (R /* h)) . n))) by A32, A35, A33, A34

          .= ((((h " ) (#) (R1 /* h)) . n) + (( - ((h " ) (#) (R /* h))) . n)) by VALUED_1: 8

          .= ((((h " ) (#) (R1 /* h)) + ( - ((h " ) (#) (R /* h)))) . n) by A30, VALUED_1: 1;

        end;

        then (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) is constant & ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1) = (a - b) by VALUED_0:def 18, A27;

        then

         A36: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (a - b) by CFCONT_1: 28;

        

         A37: ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0 by Def3;

        ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0 by Def3;

        then (a - b) = ( 0 - 0 ) by A36, A37, COMSEQ_2: 26;

        hence thesis;

      end;

    end

    definition

      let f;

      :: CFDIFF_1:def8

      attr f is differentiable means for x st x in ( dom f) holds f is_differentiable_in x;

    end

    definition

      let f, X;

      :: CFDIFF_1:def9

      pred f is_differentiable_on X means X c= ( dom f) & (f | X) is differentiable;

    end

    theorem :: CFDIFF_1:8

    

     Th8: f is_differentiable_on X implies X is Subset of COMPLEX by XBOOLE_1: 1;

    definition

      let X be Subset of COMPLEX ;

      :: CFDIFF_1:def10

      attr X is closed means for s1 be Complex_Sequence st ( rng s1) c= X & s1 is convergent holds ( lim s1) in X;

    end

    definition

      let X be Subset of COMPLEX ;

      :: CFDIFF_1:def11

      attr X is open means (X ` ) is closed;

    end

    theorem :: CFDIFF_1:9

    

     Th9: for X be Subset of COMPLEX st X is open holds for z0 be Complex st z0 in X holds ex N be Neighbourhood of z0 st N c= X

    proof

      let X be Subset of COMPLEX ;

      assume X is open;

      then

       A1: (X ` ) is closed;

      let z0 be Complex;

      assume that

       A2: z0 in X and

       A3: for N be Neighbourhood of z0 holds not N c= X;

      defpred P[ Nat, Complex] means $2 in { y where y be Complex : |.(y - z0).| < (1 / ($1 + 1)) } & $2 in (X ` );

      now

        let g be Real such that

         A4: 0 < g;

        set N = { y where y be Complex : |.(y - z0).| < g };

        N is Neighbourhood of z0 by A4, Th6;

        then not N c= X by A3;

        then

        consider x be object such that

         A5: x in N and

         A6: not x in X;

        consider s be Complex such that

         A7: x = s and

         A8: |.(s - z0).| < g by A5;

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

        take s;

        thus s in N by A8;

        thus s in (X ` ) by A6, A7, XBOOLE_0:def 5;

      end;

      then

       A9: for n be Element of NAT holds ex s be Element of COMPLEX st P[n, s];

      consider s1 be sequence of COMPLEX such that

       A10: for n be Element of NAT holds P[n, (s1 . n)] from FUNCT_2:sch 3( A9);

      

       A11: ( rng s1) c= (X ` )

      proof

        let y be object;

        assume y in ( rng s1);

        then

        consider y1 be object such that

         A12: y1 in ( dom s1) and

         A13: (s1 . y1) = y by FUNCT_1:def 3;

        reconsider y1 as Element of NAT by A12;

        (s1 . y1) in (X ` ) by A10;

        hence thesis by A13;

      end;

       A14:

      now

        let p be Real;

        assume

         A15: 0 < p;

        consider n such that

         A16: (p " ) < n by SEQ_4: 3;

        take n;

        let m be Nat;

        assume n <= m;

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

        then

         A17: (1 / (m + 1)) <= (1 / (n + 1)) by XREAL_1: 118;

        m in NAT by ORDINAL1:def 12;

        then (s1 . m) in { y where y be Complex : |.(y - z0).| < (1 / (m + 1)) } by A10;

        then ex y be Complex st (s1 . m) = y & |.(y - z0).| < (1 / (m + 1));

        then

         A18: |.((s1 . m) - z0).| < (1 / (n + 1)) by A17, XXREAL_0: 2;

        ((p " ) + 0 ) < (n + 1) by A16, XREAL_1: 8;

        then (1 / (n + 1)) < (1 / (p " )) by A15, XREAL_1: 76;

        hence |.((s1 . m) - z0).| < p by A18, XXREAL_0: 2;

      end;

      then

       A19: s1 is convergent;

      then ( lim s1) = z0 by A14, COMSEQ_2:def 6;

      then z0 in ( COMPLEX \ X) by A19, A11, A1;

      hence contradiction by A2, XBOOLE_0:def 5;

    end;

    theorem :: CFDIFF_1:10

    for X be Subset of COMPLEX st X is open holds for z0 be Complex st z0 in X holds ex g be Real st { y where y be Complex : |.(y - z0).| < g } c= X

    proof

      let X be Subset of COMPLEX such that

       A1: X is open;

      let z0 be Complex;

      assume z0 in X;

      then

      consider N be Neighbourhood of z0 such that

       A2: N c= X by A1, Th9;

      consider g be Real such that 0 < g and

       A3: { y where y be Complex : |.(y - z0).| < g } c= N by Def5;

      take g;

      thus thesis by A2, A3;

    end;

    theorem :: CFDIFF_1:11

    

     Th11: for X be Subset of COMPLEX holds ((for z0 be Complex st z0 in X holds ex N be Neighbourhood of z0 st N c= X) implies X is open)

    proof

      let X be Subset of COMPLEX ;

      assume that

       A1: for z0 be Complex st z0 in X holds ex N be Neighbourhood of z0 st N c= X and

       A2: not X is open;

       not (X ` ) is closed by A2;

      then

      consider s1 be sequence of COMPLEX such that

       A3: ( rng s1) c= (X ` ) and

       A4: s1 is convergent and

       A5: not ( lim s1) in (X ` );

      ( lim s1) in COMPLEX by XCMPLX_0:def 2;

      then ( lim s1) in X by A5, SUBSET_1: 29;

      then

      consider N be Neighbourhood of ( lim s1) such that

       A6: N c= X by A1;

      consider g be Real such that

       A7: 0 < g and

       A8: { y where y be Complex : |.(y - ( lim s1)).| < g } c= N by Def5;

      consider n such that

       A9: for m be Nat st n <= m holds |.((s1 . m) - ( lim s1)).| < g by A4, A7, COMSEQ_2:def 6;

      n in NAT by ORDINAL1:def 12;

      then n in ( dom s1) by FUNCT_2:def 1;

      then

       A10: (s1 . n) in ( rng s1) by FUNCT_1:def 3;

       |.((s1 . n) - ( lim s1)).| < g by A9;

      then (s1 . n) in { y where y be Complex : |.(y - ( lim s1)).| < g };

      then (s1 . n) in N by A8;

      hence contradiction by A3, A6, A10, XBOOLE_0:def 5;

    end;

    theorem :: CFDIFF_1:12

    for X be Subset of COMPLEX holds X is open iff for x be Complex st x in X holds ex N be Neighbourhood of x st N c= X by Th9, Th11;

    theorem :: CFDIFF_1:13

    

     Th13: for X be Subset of COMPLEX , z0 be Element of COMPLEX , r be Real st X = { y where y be Complex : |.(y - z0).| < r } holds X is open

    proof

      let X be Subset of COMPLEX , z0 be Element of COMPLEX , r be Real;

      reconsider X0 = X as Subset of COMPLEX ;

      assume

       A1: X = { y where y be Complex : |.(y - z0).| < r };

      for x be Complex st x in X0 holds ex N be Neighbourhood of x st N c= X0

      proof

        let x be Complex;

        reconsider r1 = ((r - |.(x - z0).|) / 2) as Real;

        set N = { y where y be Complex : |.(y - x).| < r1 };

        assume x in X0;

        then ex y be Complex st x = y & |.(y - z0).| < r by A1;

        then

         A2: (r - |.(x - z0).|) > 0 by XREAL_1: 50;

        then

        reconsider N as Neighbourhood of x by Th6;

        r1 < (r - |.(x - z0).|) by A2, XREAL_1: 216;

        then

         A3: (r1 + |.(x - z0).|) < ((r - |.(x - z0).|) + |.(x - z0).|) by XREAL_1: 8;

        take N;

        let z be object;

        assume z in N;

        then

        consider y1 be Complex such that

         A4: z = y1 and

         A5: |.(y1 - x).| < r1;

        ( |.(y1 - x).| + |.(x - z0).|) < (r1 + |.(x - z0).|) by A5, XREAL_1: 8;

        then |.(y1 - z0).| <= ( |.(y1 - x).| + |.(x - z0).|) & ( |.(y1 - x).| + |.(x - z0).|) < r by A3, COMPLEX1: 63, XXREAL_0: 2;

        then |.(y1 - z0).| < r by XXREAL_0: 2;

        hence thesis by A1, A4;

      end;

      hence thesis by Th11;

    end;

    theorem :: CFDIFF_1:14

    for X be Subset of COMPLEX , z0 be Element of COMPLEX , r be Real st X = { y where y be Complex : |.(y - z0).| <= r } holds X is closed

    proof

      let X be Subset of COMPLEX , z0 be Element of COMPLEX , r be Real;

      reconsider X0 = X as Subset of COMPLEX ;

      assume

       A1: X = { y where y be Complex : |.(y - z0).| <= r };

      for s1 be Complex_Sequence st ( rng s1) c= X0 & s1 is convergent holds ( lim s1) in X0

      proof

        reconsider r as Element of REAL by XREAL_0:def 1;

        set s4 = ( seq_const r);

        reconsider s2 = ( NAT --> z0) as Complex_Sequence;

        let s1 be Complex_Sequence;

        assume that

         A2: ( rng s1) c= X0 and

         A3: s1 is convergent;

        set s3 = (s1 - s2);

        

         A4: s2 is convergent by CFCONT_1: 26;

        then

         A5: ( lim s3) = (( lim s1) - ( lim s2)) by A3, COMSEQ_2: 26;

        

         A6: for n be Element of NAT holds ( |.s3.| . n) <= r

        proof

          let n be Element of NAT ;

          now

            let n be Element of NAT ;

            (s3 . n) = ((s1 . n) + (( - s2) . n)) by VALUED_1: 1

            .= ((s1 . n) - (s2 . n)) by VALUED_1: 8;

            hence (s3 . n) = ((s1 . n) - z0);

          end;

          then

           A7: (s3 . n) = ((s1 . n) - z0);

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

          then (s1 . n) in ( rng s1) by FUNCT_1:def 3;

          then (s1 . n) in X0 by A2;

          then ex y be Complex st y = (s1 . n) & |.(y - z0).| <= r by A1;

          hence thesis by A7, VALUED_1: 18;

        end;

        s3 is convergent by A3, A4;

        then

         A8: ( lim |.s3.|) = |.( lim s3).| by SEQ_2: 27;

        reconsider s3 = (s1 - s2) as convergent Complex_Sequence by A3, A4;

        

         A9: for n be Nat holds ( |.s3.| . n) <= (s4 . n)

        proof

          let n be Nat;

          

           A10: n in NAT by ORDINAL1:def 12;

          ( |.s3.| . n) <= r by A6, A10;

          hence thesis by SEQ_1: 57;

        end;

        

         A11: for n be Element of NAT holds ( lim s2) = z0

        proof

          let n be Element of NAT ;

          ( lim s2) = (s2 . n) by CFCONT_1: 28

          .= z0;

          hence thesis;

        end;

        ( lim s4) = (s4 . 0 ) by SEQ_4: 26

        .= r by SEQ_1: 57;

        then ( lim |.s3.|) <= r by A9, SEQ_2: 18;

        then |.(( lim s1) - z0).| <= r by A11, A5, A8;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    registration

      cluster open for Subset of COMPLEX ;

      existence

      proof

        reconsider X = { y where y be Complex : |.(y - 0c ).| < 1 } as Subset of COMPLEX by Th6;

        X is open by Th13;

        hence thesis;

      end;

    end

    reserve Z for open Subset of COMPLEX ;

    theorem :: CFDIFF_1:15

    

     Th15: f is_differentiable_on Z iff Z c= ( dom f) & for x st x in Z holds f is_differentiable_in x

    proof

      thus f is_differentiable_on Z implies Z c= ( dom f) & for x st x in Z holds f is_differentiable_in x

      proof

        assume

         A1: f is_differentiable_on Z;

        hence

         A2: Z c= ( dom f);

        let x0;

        

         A3: (f | Z) is differentiable by A1;

        assume

         A4: x0 in Z;

        then x0 in ( dom (f | Z)) by A2, RELAT_1: 57;

        then (f | Z) is_differentiable_in x0 by A3;

        then

        consider N be Neighbourhood of x0 such that

         A5: N c= ( dom (f | Z)) and

         A6: ex L, R st for x st x in N holds (((f | Z) /. x) - ((f | Z) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

        take N;

        ( dom (f | Z)) = (( dom f) /\ Z) by RELAT_1: 61;

        then ( dom (f | Z)) c= ( dom f) by XBOOLE_1: 17;

        hence N c= ( dom f) by A5;

        consider L, R such that

         A7: for x st x in N holds (((f | Z) /. x) - ((f | Z) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A6;

        take L, R;

        let x;

        assume

         A8: x in N;

        then (((f | Z) /. x) - ((f | Z) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A7;

        then

         A9: ((f /. x) - ((f | Z) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A5, A8, PARTFUN2: 15;

        x0 in (( dom f) /\ Z) by A2, A4, XBOOLE_0:def 4;

        hence thesis by A9, PARTFUN2: 16;

      end;

      assume that

       A10: Z c= ( dom f) and

       A11: for x st x in Z holds f is_differentiable_in x;

      thus Z c= ( dom f) by A10;

      let x0;

      assume x0 in ( dom (f | Z));

      then

       A12: x0 in Z by RELAT_1: 57;

      then

      consider N1 be Neighbourhood of x0 such that

       A13: N1 c= Z by Th9;

      f is_differentiable_in x0 by A11, A12;

      then

      consider N be Neighbourhood of x0 such that

       A14: N c= ( dom f) and

       A15: ex L, R st for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

      consider N2 be Neighbourhood of x0 such that

       A16: N2 c= N1 and

       A17: N2 c= N by Lm1;

      

       A18: N2 c= Z by A13, A16;

      take N2;

      N2 c= ( dom f) by A14, A17;

      then N2 c= (( dom f) /\ Z) by A18, XBOOLE_1: 19;

      hence

       A19: N2 c= ( dom (f | Z)) by RELAT_1: 61;

      consider L, R such that

       A20: for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A15;

      

       A21: x0 in N2 by Th7;

      take L, R;

      let x;

      assume

       A22: x in N2;

      then ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A17, A20;

      then (((f | Z) /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A19, A22, PARTFUN2: 15;

      hence thesis by A19, A21, PARTFUN2: 15;

    end;

    theorem :: CFDIFF_1:16

    f is_differentiable_on Y implies Y is open

    proof

      assume

       A1: f is_differentiable_on Y;

      then

       A2: Y c= ( dom f);

      now

        let x0 be Complex;

        assume x0 in Y;

        then

         A3: x0 in ( dom (f | Y)) by A2, RELAT_1: 57;

        (f | Y) is differentiable by A1;

        then (f | Y) is_differentiable_in x0 by A3;

        then

        consider N be Neighbourhood of x0 such that

         A4: N c= ( dom (f | Y)) and ex L, R st for x st x in N holds (((f | Y) /. x) - ((f | Y) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

        take N;

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

        then ( dom (f | Y)) c= Y by XBOOLE_1: 17;

        hence N c= Y by A4;

      end;

      hence thesis by Th11;

    end;

    definition

      let f, X;

      assume

       A1: f is_differentiable_on X;

      :: CFDIFF_1:def12

      func f `| X -> PartFunc of COMPLEX , COMPLEX means

      : Def12: ( dom it ) = X & for x st x in X holds (it /. x) = ( diff (f,x));

      existence

      proof

        deffunc F( Element of COMPLEX ) = ( diff (f,$1));

        defpred P[ set] means $1 in X;

        consider F be PartFunc of COMPLEX , COMPLEX such that

         A2: (for x be Element of COMPLEX holds x in ( dom F) iff P[x]) & for x be Element of COMPLEX st x in ( dom F) holds (F . x) = F(x) from SEQ_1:sch 3;

        take F;

        now

          

           A3: X is Subset of COMPLEX by A1, Th8;

          let y be object;

          assume y in X;

          hence y in ( dom F) by A2, A3;

        end;

        then

         A4: X c= ( dom F);

        for y be object st y in ( dom F) holds y in X by A2;

        then ( dom F) c= X;

        hence ( dom F) = X by A4;

        now

          let x;

          assume

           A5: x in X;

          x in COMPLEX by XCMPLX_0:def 2;

          then

           A6: x in ( dom F) by A2, A5;

          then (F . x) = ( diff (f,x)) by A2;

          hence (F /. x) = ( diff (f,x)) by A6, PARTFUN1:def 6;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be PartFunc of COMPLEX , COMPLEX ;

        assume that

         A7: ( dom F) = X and

         A8: for x st x in X holds (F /. x) = ( diff (f,x)) and

         A9: ( dom G) = X and

         A10: for x st x in X holds (G /. x) = ( diff (f,x));

        now

          let x be Element of COMPLEX ;

          assume

           A11: x in ( dom F);

          then (F /. x) = ( diff (f,x)) by A7, A8;

          hence (F /. x) = (G /. x) by A7, A10, A11;

        end;

        hence thesis by A7, A9, PARTFUN2: 1;

      end;

    end

    theorem :: CFDIFF_1:17

    for f, Z st Z c= ( dom f) & ex a1 st ( rng f) = {a1} holds f is_differentiable_on Z & for x st x in Z holds ((f `| Z) /. x) = 0c

    proof

      reconsider cf = ( COMPLEX --> 0c ) as Function of COMPLEX , COMPLEX ;

      set R = cf;

      now

        let h;

        now

          let n be Nat;

          

           A2: ( rng h) c= ( dom R) & n in NAT by ORDINAL1:def 12;

          

          thus (((h " ) (#) (R /* h)) . n) = (((h " ) . n) * ((R /* h) . n)) by VALUED_1: 5

          .= (((h " ) . n) * (R /. (h . n))) by A2, FUNCT_2: 109

          .= (((h " ) . n) * 0c )

          .= 0c ;

        end;

        then ((h " ) (#) (R /* h)) is constant & (((h " ) (#) (R /* h)) . 0 ) = 0c by VALUED_0:def 18;

        hence ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0c by CFCONT_1: 26, CFCONT_1: 27;

      end;

      then

      reconsider R as C_RestFunc by Def3;

      set L = cf;

      for z holds (L /. z) = ( 0c * z) by XCMPLX_0:def 2, FUNCOP_1: 7;

      then

      reconsider L as C_LinearFunc by Def4;

      let f, Z such that

       A3: Z c= ( dom f);

      given a1 such that

       A4: ( rng f) = {a1};

       A5:

      now

        let x0;

        assume

         A6: x0 in ( dom f);

        then (f . x0) in {a1} by A4, FUNCT_1:def 3;

        then (f /. x0) in {a1} by A6, PARTFUN1:def 6;

        hence (f /. x0) = a1 by TARSKI:def 1;

      end;

       A7:

      now

        let x0;

        assume

         A8: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A9: N c= Z by Th9;

        

         A10: N c= ( dom f) by A3, A9;

        

         A11: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

        proof

          let x;

          assume x in N;

          

          hence ((f /. x) - (f /. x0)) = (a1 - (f /. x0)) by A5, A10

          .= (a1 - a1) by A3, A5, A8

          .= ((L /. (x - x0)) + 0c ) by FUNCOP_1: 7, A11

          .= ((L /. (x - x0)) + (R /. (x - x0))) by FUNCOP_1: 7, A11;

        end;

        hence f is_differentiable_in x0 by A10;

      end;

      hence

       A12: f is_differentiable_on Z by A3, Th15;

      let x0;

      assume

       A13: x0 in Z;

      then

       A14: f is_differentiable_in x0 by A7;

      then ex N be Neighbourhood of x0 st N c= ( dom f) & ex L, R st for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

      then

      consider N be Neighbourhood of x0 such that

       A15: N c= ( dom f);

      

       A16: for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

      proof

        let x;

        

         A17: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        assume x in N;

        

        hence ((f /. x) - (f /. x0)) = (a1 - (f /. x0)) by A5, A15

        .= (a1 - a1) by A3, A5, A13

        .= ((L /. (x - x0)) + 0c ) by FUNCOP_1: 7, A17

        .= ((L /. (x - x0)) + (R /. (x - x0))) by FUNCOP_1: 7, A17;

      end;

      

      thus ((f `| Z) /. x0) = ( diff (f,x0)) by A12, A13, Def12

      .= (L /. 1r ) by A14, A15, A16, Def7

      .= 0c ;

    end;

    registration

      let seq be non-zero Complex_Sequence, k be Nat;

      cluster (seq ^\ k) -> non-zero;

      coherence

      proof

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

        now

          let n be Element of NAT ;

          ((seq ^\ k) . n) = (seq . (n + k)) by NAT_1:def 3;

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

        end;

        hence thesis by COMSEQ_1: 4;

      end;

    end

    registration

      let h, n;

      cluster (h ^\ n) -> 0 -convergent;

      coherence

      proof

        ( lim h) = 0 by Def1;

        then

         A1: ( lim (h ^\ n)) = 0 by CFCONT_1: 21;

        (h ^\ n) is convergent by CFCONT_1: 21;

        hence thesis by A1;

      end;

    end

    theorem :: CFDIFF_1:18

    

     Th18: ((seq + seq1) ^\ k) = ((seq ^\ k) + (seq1 ^\ k))

    proof

      now

        let n be Element of NAT ;

        

         A1: (n + k) in NAT by ORDINAL1:def 12;

        

        thus (((seq + seq1) ^\ k) . n) = ((seq + seq1) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) + (seq1 . (n + k))) by VALUED_1: 1, A1

        .= (((seq ^\ k) . n) + (seq1 . (n + k))) by NAT_1:def 3

        .= (((seq ^\ k) . n) + ((seq1 ^\ k) . n)) by NAT_1:def 3

        .= (((seq ^\ k) + (seq1 ^\ k)) . n) by VALUED_1: 1;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:19

    

     Th19: ((seq - seq1) ^\ k) = ((seq ^\ k) - (seq1 ^\ k))

    proof

      now

        let n be Element of NAT ;

        

         A1: (n + k) in NAT by ORDINAL1:def 12;

        

        thus (((seq - seq1) ^\ k) . n) = ((seq + ( - seq1)) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) + (( - seq1) . (n + k))) by VALUED_1: 1, A1

        .= ((seq . (n + k)) + ( - (seq1 . (n + k)))) by VALUED_1: 8

        .= (((seq ^\ k) . n) - (seq1 . (n + k))) by NAT_1:def 3

        .= (((seq ^\ k) . n) + ( - ((seq1 ^\ k) . n))) by NAT_1:def 3

        .= (((seq ^\ k) . n) + (( - (seq1 ^\ k)) . n)) by VALUED_1: 8

        .= (((seq ^\ k) - (seq1 ^\ k)) . n) by VALUED_1: 1;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:20

    

     Th20: ((seq " ) ^\ k) = ((seq ^\ k) " )

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq " ) ^\ k) . n) = ((seq " ) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) " ) by VALUED_1: 10

        .= (((seq ^\ k) . n) " ) by NAT_1:def 3

        .= (((seq ^\ k) " ) . n) by VALUED_1: 10;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:21

    

     Th21: ((seq (#) seq1) ^\ k) = ((seq ^\ k) (#) (seq1 ^\ k))

    proof

      now

        let n be Element of NAT ;

        

        thus (((seq (#) seq1) ^\ k) . n) = ((seq (#) seq1) . (n + k)) by NAT_1:def 3

        .= ((seq . (n + k)) * (seq1 . (n + k))) by VALUED_1: 5

        .= (((seq ^\ k) . n) * (seq1 . (n + k))) by NAT_1:def 3

        .= (((seq ^\ k) . n) * ((seq1 ^\ k) . n)) by NAT_1:def 3

        .= (((seq ^\ k) (#) (seq1 ^\ k)) . n) by VALUED_1: 5;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:22

    

     Th22: for x0 be Complex holds for N be Neighbourhood of x0 st f is_differentiable_in x0 & N c= ( dom f) holds for h, c st ( rng c) = {x0} & ( rng (h + c)) c= N holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( diff (f,x0)) = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))))

    proof

      let x0 be Complex;

      let N be Neighbourhood of x0;

      assume that

       A1: f is_differentiable_in x0 and

       A2: N c= ( dom f);

      consider N1 be Neighbourhood of x0 such that N1 c= ( dom f) and

       A3: ex L, R st for x st x in N1 holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A1;

      consider N2 be Neighbourhood of x0 such that

       A4: N2 c= N and

       A5: N2 c= N1 by Lm1;

      

       A6: N2 c= ( dom f) by A2, A4;

      let h, c such that

       A7: ( rng c) = {x0} and

       A8: ( rng (h + c)) c= N;

      consider g be Real such that

       A9: 0 < g and

       A10: { y where y be Complex : |.(y - x0).| < g } c= N2 by Def5;

       |.(x0 - x0).| = 0 by COMPLEX1: 44;

      then x0 in { y where y be Complex : |.(y - x0).| < g } by A9;

      then

       A11: x0 in N2 by A10;

      

       A12: ( rng c) c= ( dom f)

      proof

        let y be object;

        assume y in ( rng c);

        then y = x0 by A7, TARSKI:def 1;

        then y in N by A4, A11;

        hence thesis by A2;

      end;

      ex n st ( rng (c ^\ n)) c= N2 & ( rng ((h + c) ^\ n)) c= N2

      proof

        x0 in ( rng c) by A7, TARSKI:def 1;

        then

         A13: ( lim c) = x0 by CFCONT_1: 27;

        

         A14: c is convergent by CFCONT_1: 26;

        then

         A15: (h + c) is convergent;

        ( lim h) = 0 by Def1;

        

        then ( lim (h + c)) = ( 0 + x0) by A14, A13, COMSEQ_2: 14

        .= x0;

        then

        consider n such that

         A16: for m be Nat st n <= m holds |.(((h + c) . m) - x0).| < g by A9, A15, COMSEQ_2:def 6;

        take n;

        

         A17: ( rng (c ^\ n)) = {x0} by A7, VALUED_0: 26;

        thus ( rng (c ^\ n)) c= N2 by A11, A17, TARSKI:def 1;

        let y be object;

        assume y in ( rng ((h + c) ^\ n));

        then

        consider m be Element of NAT such that

         A18: y = (((h + c) ^\ n) . m) by FUNCT_2: 113;

        reconsider y1 = y as Complex by A18;

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

        then |.(((h + c) . (n + m)) - x0).| < g by A16;

        then |.((((h + c) ^\ n) . m) - x0).| < g by NAT_1:def 3;

        then y1 in { z where z be Complex : |.(z - x0).| < g } by A18;

        hence thesis by A10;

      end;

      then

      consider n such that ( rng (c ^\ n)) c= N2 and

       A19: ( rng ((h + c) ^\ n)) c= N2;

      consider L, R such that

       A20: for x st x in N1 holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A3;

      

       A21: ( rng (c ^\ n)) c= ( dom f)

      proof

        let y be object;

        assume

         A22: y in ( rng (c ^\ n));

        ( rng (c ^\ n)) = ( rng c) by VALUED_0: 26;

        then y = x0 by A7, A22, TARSKI:def 1;

        then y in N by A4, A11;

        hence thesis by A2;

      end;

      

       A23: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent & ( lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ))) = (L /. 1r )

      proof

        deffunc F( Nat) = ((L /. 1r ) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . $1));

        consider s1 such that

         A24: for k holds (s1 . k) = F(k) from COMSEQ_1:sch 1;

         A25:

        now

          

           A26: (((h ^\ n) " ) (#) (R /* (h ^\ n))) is convergent & ( lim (((h ^\ n) " ) (#) (R /* (h ^\ n)))) = 0 by Def3;

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

           A27: for k be Nat st m <= k holds |.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0c ).| < r by A26, COMSEQ_2:def 6;

          take n1 = m;

          let k such that

           A28: n1 <= k;

           |.((s1 . k) - (L /. 1r )).| = |.(((L /. 1r ) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . k)) - (L /. 1r )).| by A24

          .= |.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0c ).|;

          hence |.((s1 . k) - (L /. 1r )).| < r by A27, A28;

        end;

        consider x such that

         A29: for b1 holds (L /. b1) = (x * b1) by Def4;

        

         A30: (L /. 1r ) = (x * 1r ) by A29

        .= x;

        now

          let m be Element of NAT ;

          

           A31: ((h ^\ n) . m) <> 0c by COMSEQ_1: 4;

          

          thus ((((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) . m) = ((((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) " ) . m)) by VALUED_1: 5

          .= ((((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) " ) . m)) by VALUED_1: 1

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)))

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by VALUED_1: 5

          .= ((((L /* (h ^\ n)) . m) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by VALUED_1: 10

          .= (((L /. ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by FUNCT_2: 115

          .= (((x * ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A29

          .= ((x * (((h ^\ n) . m) * (((h ^\ n) . m) " ))) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m))

          .= ((x * 1r ) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)) by A31, XCMPLX_0:def 7

          .= (s1 . m) by A24, A30;

        end;

        then

         A32: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = s1;

        hence (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent by A25;

        hence thesis by A32, A25, COMSEQ_2:def 6;

      end;

      

       A33: for k holds ((f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k))) = ((L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)))

      proof

        let k;

        

         A34: (k + n) in NAT by ORDINAL1:def 12;

        

         A35: k in NAT by ORDINAL1:def 12;

        then (((h + c) ^\ n) . k) in ( rng ((h + c) ^\ n)) by FUNCT_2: 112;

        then

         A36: (((h + c) ^\ n) . k) in N2 by A19;

        ((c ^\ n) . k) in ( rng (c ^\ n)) & ( rng (c ^\ n)) = ( rng c) by FUNCT_2: 112, VALUED_0: 26, A35;

        then

         A37: ((c ^\ n) . k) = x0 by A7, TARSKI:def 1;

        ((((h + c) ^\ n) . k) - ((c ^\ n) . k)) = (((h + c) . (k + n)) - ((c ^\ n) . k)) by NAT_1:def 3

        .= (((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k)) by VALUED_1: 1, A34

        .= ((((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k)) by NAT_1:def 3

        .= ((((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k)) by NAT_1:def 3

        .= ((h ^\ n) . k);

        hence thesis by A20, A5, A36, A37;

      end;

      

       A38: ( rng (h + c)) c= ( dom f) by A8, A2;

      

       A39: ( rng ((h + c) ^\ n)) c= ( dom f) by A19, A4, A2;

      now

        let k be Element of NAT ;

        

        thus (((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k) = (((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k)) by CFCONT_1: 1

        .= ((f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k)) by A39, FUNCT_2: 109

        .= ((f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k))) by A21, FUNCT_2: 109

        .= ((L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))) by A33

        .= (((L /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k))) by FUNCT_2: 115

        .= (((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k)) by FUNCT_2: 115

        .= (((L /* (h ^\ n)) + (R /* (h ^\ n))) . k) by VALUED_1: 1;

      end;

      

      then

       A40: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = (((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) (#) ((h ^\ n) " )) by FUNCT_2:def 7

      .= ((((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) " )) by A38, VALUED_0: 27

      .= ((((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) (#) ((h ^\ n) " )) by A12, VALUED_0: 27

      .= ((((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ^\ n) " )) by Th19

      .= ((((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h " ) ^\ n)) by Th20

      .= ((((f /* (h + c)) - (f /* c)) (#) (h " )) ^\ n) by Th21;

      then

       A41: (L /. 1r ) = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) by A23, CFCONT_1: 23;

      thus ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A23, A40, CFCONT_1: 22;

      for x st x in N2 holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A20, A5;

      hence thesis by A1, A6, A41, Def7;

    end;

    theorem :: CFDIFF_1:23

    

     Th23: for f1, f2, x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds (f1 + f2) is_differentiable_in x0 & ( diff ((f1 + f2),x0)) = (( diff (f1,x0)) + ( diff (f2,x0)))

    proof

      let f1, f2, x0;

      assume that

       A1: f1 is_differentiable_in x0 and

       A2: f2 is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A3: N1 c= ( dom f1) and

       A4: ex L, R st for x st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A1;

      consider L1, R1 such that

       A5: for x st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A4;

      consider N2 be Neighbourhood of x0 such that

       A6: N2 c= ( dom f2) and

       A7: ex L, R st for x st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A2;

      consider L2, R2 such that

       A8: for x st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L2 /. (x - x0)) + (R2 /. (x - x0))) by A7;

      reconsider R = (R1 + R2) as C_RestFunc;

      reconsider L = (L1 + L2) as C_LinearFunc;

      consider N be Neighbourhood of x0 such that

       A9: N c= N1 and

       A10: N c= N2 by Lm1;

      

       A11: N c= ( dom f2) by A6, A10;

      N c= ( dom f1) by A3, A9;

      then (N /\ N) c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 27;

      then

       A12: N c= ( dom (f1 + f2)) by VALUED_1:def 1;

       A13:

      now

        let x;

        

         A14: x0 in N by Th7;

        

         A15: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        assume

         A16: x in N;

        

        hence (((f1 + f2) /. x) - ((f1 + f2) /. x0)) = (((f1 /. x) + (f2 /. x)) - ((f1 + f2) /. x0)) by A12, CFUNCT_1: 1

        .= (((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0))) by A12, A14, CFUNCT_1: 1

        .= (((f1 /. x) - (f1 /. x0)) + ((f2 /. x) - (f2 /. x0)))

        .= (((L1 /. (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0))) by A5, A9, A16

        .= (((L1 /. (x - x0)) + (R1 /. (x - x0))) + ((L2 /. (x - x0)) + (R2 /. (x - x0)))) by A8, A10, A16

        .= (((L1 /. (x - x0)) + (L2 /. (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0))))

        .= ((L /. (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((L /. (x - x0)) + (R /. (x - x0))) by CFUNCT_1: 64, A15;

      end;

      hence (f1 + f2) is_differentiable_in x0 by A12;

      

      hence ( diff ((f1 + f2),x0)) = (L /. 1r ) by A12, A13, Def7

      .= ((L1 /. 1r ) + (L2 /. 1r )) by CFUNCT_1: 64

      .= (( diff (f1,x0)) + (L2 /. 1r )) by A1, A3, A5, Def7

      .= (( diff (f1,x0)) + ( diff (f2,x0))) by A2, A6, A8, Def7;

    end;

    theorem :: CFDIFF_1:24

    

     Th24: for f1, f2, x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds (f1 - f2) is_differentiable_in x0 & ( diff ((f1 - f2),x0)) = (( diff (f1,x0)) - ( diff (f2,x0)))

    proof

      let f1, f2, x0;

      assume that

       A1: f1 is_differentiable_in x0 and

       A2: f2 is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A3: N1 c= ( dom f1) and

       A4: ex L, R st for x st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A1;

      consider L1, R1 such that

       A5: for x st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A4;

      consider N2 be Neighbourhood of x0 such that

       A6: N2 c= ( dom f2) and

       A7: ex L, R st for x st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A2;

      consider L2, R2 such that

       A8: for x st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L2 /. (x - x0)) + (R2 /. (x - x0))) by A7;

      reconsider R = (R1 - R2) as C_RestFunc;

      reconsider L = (L1 - L2) as C_LinearFunc;

      consider N be Neighbourhood of x0 such that

       A9: N c= N1 and

       A10: N c= N2 by Lm1;

      

       A11: N c= ( dom f2) by A6, A10;

      N c= ( dom f1) by A3, A9;

      then (N /\ N) c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 27;

      then

       A12: N c= ( dom (f1 - f2)) by CFUNCT_1: 2;

       A13:

      now

        let x;

        

         A14: x0 in N by Th7;

        

         A15: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        assume

         A16: x in N;

        

        hence (((f1 - f2) /. x) - ((f1 - f2) /. x0)) = (((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. x0)) by A12, CFUNCT_1: 2

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

        .= (((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0)))

        .= (((L1 /. (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0))) by A5, A9, A16

        .= (((L1 /. (x - x0)) + (R1 /. (x - x0))) - ((L2 /. (x - x0)) + (R2 /. (x - x0)))) by A8, A10, A16

        .= (((L1 /. (x - x0)) - (L2 /. (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0))))

        .= ((L /. (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((L /. (x - x0)) + (R /. (x - x0))) by CFUNCT_1: 64, A15;

      end;

      hence (f1 - f2) is_differentiable_in x0 by A12;

      

      hence ( diff ((f1 - f2),x0)) = (L /. 1r ) by A12, A13, Def7

      .= ((L1 /. 1r ) - (L2 /. 1r )) by CFUNCT_1: 64

      .= (( diff (f1,x0)) - (L2 /. 1r )) by A1, A3, A5, Def7

      .= (( diff (f1,x0)) - ( diff (f2,x0))) by A2, A6, A8, Def7;

    end;

    theorem :: CFDIFF_1:25

    

     Th25: for a, f, x0 st f is_differentiable_in x0 holds (a (#) f) is_differentiable_in x0 & ( diff ((a (#) f),x0)) = (a * ( diff (f,x0)))

    proof

      let a, f, x0;

      assume

       A1: f is_differentiable_in x0;

      then

      consider N1 be Neighbourhood of x0 such that

       A2: N1 c= ( dom f) and

       A3: ex L, R st for x st x in N1 holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

      consider L1, R1 such that

       A4: for x st x in N1 holds ((f /. x) - (f /. x0)) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A3;

      reconsider R = (a (#) R1) as C_RestFunc;

      reconsider L = (a (#) L1) as C_LinearFunc;

      

       A5: N1 c= ( dom (a (#) f)) by A2, VALUED_1:def 5;

       A6:

      now

        let x;

        

         A7: x0 in N1 by Th7;

        

         A8: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        assume

         A9: x in N1;

        

        hence (((a (#) f) /. x) - ((a (#) f) /. x0)) = ((a * (f /. x)) - ((a (#) f) /. x0)) by A5, CFUNCT_1: 4

        .= ((a * (f /. x)) - (a * (f /. x0))) by A5, A7, CFUNCT_1: 4

        .= (a * ((f /. x) - (f /. x0)))

        .= (a * ((L1 /. (x - x0)) + (R1 /. (x - x0)))) by A4, A9

        .= ((a * (L1 /. (x - x0))) + (a * (R1 /. (x - x0))))

        .= ((L /. (x - x0)) + (a * (R1 /. (x - x0)))) by CFUNCT_1: 65, A8

        .= ((L /. (x - x0)) + (R /. (x - x0))) by CFUNCT_1: 65, A8;

      end;

      hence (a (#) f) is_differentiable_in x0 by A5;

      

      hence ( diff ((a (#) f),x0)) = (L /. 1r ) by A5, A6, Def7

      .= (a * (L1 /. 1r )) by CFUNCT_1: 65

      .= (a * ( diff (f,x0))) by A1, A2, A4, Def7;

    end;

    theorem :: CFDIFF_1:26

    

     Th26: for f1, f2, x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds (f1 (#) f2) is_differentiable_in x0 & ( diff ((f1 (#) f2),x0)) = (((f2 /. x0) * ( diff (f1,x0))) + ((f1 /. x0) * ( diff (f2,x0))))

    proof

      let f1, f2, x0;

      assume that

       A1: f1 is_differentiable_in x0 and

       A2: f2 is_differentiable_in x0;

      consider N2 be Neighbourhood of x0 such that

       A3: N2 c= ( dom f2) and

       A4: ex L, R st for x st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A2;

      consider L2, R2 such that

       A5: for x st x in N2 holds ((f2 /. x) - (f2 /. x0)) = ((L2 /. (x - x0)) + (R2 /. (x - x0))) by A4;

      reconsider R12 = ((f1 /. x0) (#) R2) as C_RestFunc;

      reconsider L12 = ((f1 /. x0) (#) L2) as C_LinearFunc;

      consider N1 be Neighbourhood of x0 such that

       A6: N1 c= ( dom f1) and

       A7: ex L, R st for x st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A1;

      consider L1, R1 such that

       A8: for x st x in N1 holds ((f1 /. x) - (f1 /. x0)) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A7;

      reconsider R11 = ((f2 /. x0) (#) R1) as C_RestFunc;

      reconsider L11 = ((f2 /. x0) (#) L1) as C_LinearFunc;

      reconsider R18 = (R2 (#) L1) as C_RestFunc;

      reconsider R17 = (R1 (#) R2) as C_RestFunc;

      reconsider R16 = (R1 (#) L2) as C_RestFunc;

      reconsider R14 = (L1 (#) L2) as C_RestFunc;

      reconsider R13 = (R11 + R12) as C_RestFunc;

      reconsider L = (L11 + L12) as C_LinearFunc;

      reconsider R15 = (R13 + R14) as C_RestFunc;

      reconsider R19 = (R16 + R17) as C_RestFunc;

      reconsider R20 = (R19 + R18) as C_RestFunc;

      reconsider R = (R15 + R20) as C_RestFunc;

      consider N be Neighbourhood of x0 such that

       A9: N c= N1 and

       A10: N c= N2 by Lm1;

      

       A11: N c= ( dom f2) by A3, A10;

      N c= ( dom f1) by A6, A9;

      then (N /\ N) c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 27;

      then

       A12: N c= ( dom (f1 (#) f2)) by VALUED_1:def 4;

       A13:

      now

        let x;

        

         A14: x0 in N by Th7;

        

         A15: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        assume

         A16: x in N;

        then

         A17: (((f1 /. x) - (f1 /. x0)) + (f1 /. x0)) = (((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) by A8, A9;

        

        thus (((f1 (#) f2) /. x) - ((f1 (#) f2) /. x0)) = (((f1 /. x) * (f2 /. x)) - ((f1 (#) f2) /. x0)) by A12, A16, CFUNCT_1: 3

        .= (((((f1 /. x) * (f2 /. x)) + ( - ((f1 /. x) * (f2 /. x0)))) + ((f1 /. x) * (f2 /. x0))) - ((f1 /. x0) * (f2 /. x0))) by A12, A14, CFUNCT_1: 3

        .= (((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((f1 /. x) - (f1 /. x0)) * (f2 /. x0)))

        .= (((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((L1 /. (x - x0)) + (R1 /. (x - x0))) * (f2 /. x0))) by A8, A9, A16

        .= (((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((f2 /. x0) * (L1 /. (x - x0))) + ((R1 /. (x - x0)) * (f2 /. x0))))

        .= (((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + ((L11 /. (x - x0)) + ((f2 /. x0) * (R1 /. (x - x0))))) by CFUNCT_1: 65, A15

        .= (((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) * ((f2 /. x) - (f2 /. x0))) + ((L11 /. (x - x0)) + (R11 /. (x - x0)))) by A17, CFUNCT_1: 65, A15

        .= (((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L11 /. (x - x0)) + (R11 /. (x - x0)))) by A5, A10, A16

        .= (((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + (((f1 /. x0) * (L2 /. (x - x0))) + ((f1 /. x0) * (R2 /. (x - x0))))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))))

        .= (((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((f1 /. x0) * (R2 /. (x - x0))))) + ((L11 /. (x - x0)) + (R11 /. (x - x0)))) by CFUNCT_1: 65, A15

        .= (((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + (R12 /. (x - x0)))) + ((L11 /. (x - x0)) + (R11 /. (x - x0)))) by CFUNCT_1: 65, A15

        .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((L11 /. (x - x0)) + ((R11 /. (x - x0)) + (R12 /. (x - x0))))))

        .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((L11 /. (x - x0)) + (R13 /. (x - x0))))) by CFUNCT_1: 64, A15

        .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + (((L11 /. (x - x0)) + (L12 /. (x - x0))) + (R13 /. (x - x0))))

        .= (((((L1 /. (x - x0)) * (L2 /. (x - x0))) + ((L1 /. (x - x0)) * (R2 /. (x - x0)))) + ((R1 /. (x - x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((((R14 /. (x - x0)) + ((R2 /. (x - x0)) * (L1 /. (x - x0)))) + ((R1 /. (x - x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((((R14 /. (x - x0)) + (R18 /. (x - x0))) + (((R1 /. (x - x0)) * (L2 /. (x - x0))) + ((R1 /. (x - x0)) * (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((((R14 /. (x - x0)) + (R18 /. (x - x0))) + ((R16 /. (x - x0)) + ((R1 /. (x - x0)) * (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((((R14 /. (x - x0)) + (R18 /. (x - x0))) + ((R16 /. (x - x0)) + (R17 /. (x - x0)))) + ((L /. (x - x0)) + (R13 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((((R14 /. (x - x0)) + (R18 /. (x - x0))) + (R19 /. (x - x0))) + ((L /. (x - x0)) + (R13 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= (((R14 /. (x - x0)) + ((R19 /. (x - x0)) + (R18 /. (x - x0)))) + ((L /. (x - x0)) + (R13 /. (x - x0))))

        .= (((L /. (x - x0)) + (R13 /. (x - x0))) + ((R14 /. (x - x0)) + (R20 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((L /. (x - x0)) + (((R13 /. (x - x0)) + (R14 /. (x - x0))) + (R20 /. (x - x0))))

        .= ((L /. (x - x0)) + ((R15 /. (x - x0)) + (R20 /. (x - x0)))) by CFUNCT_1: 64, A15

        .= ((L /. (x - x0)) + (R /. (x - x0))) by CFUNCT_1: 64, A15;

      end;

      hence (f1 (#) f2) is_differentiable_in x0 by A12;

      

      hence ( diff ((f1 (#) f2),x0)) = (L /. 1r ) by A12, A13, Def7

      .= ((L11 /. 1r ) + (L12 /. 1r )) by CFUNCT_1: 64

      .= (((f2 /. x0) * (L1 /. 1r )) + (L12 /. 1r )) by CFUNCT_1: 65

      .= (((f2 /. x0) * (L1 /. 1r )) + ((f1 /. x0) * (L2 /. 1r ))) by CFUNCT_1: 65

      .= (((f2 /. x0) * ( diff (f1,x0))) + ((f1 /. x0) * (L2 /. 1r ))) by A1, A6, A8, Def7

      .= (((f2 /. x0) * ( diff (f1,x0))) + ((f1 /. x0) * ( diff (f2,x0)))) by A2, A3, A5, Def7;

    end;

    theorem :: CFDIFF_1:27

    for f, Z st Z c= ( dom f) & (f | Z) = ( id Z) holds f is_differentiable_on Z & for x st x in Z holds ((f `| Z) /. x) = 1r

    proof

      reconsider cf = ( COMPLEX --> 0c ) as Function of COMPLEX , COMPLEX ;

      set R = cf;

      reconsider L = ( id COMPLEX ) as PartFunc of COMPLEX , COMPLEX ;

      

       A1: COMPLEX c= COMPLEX ;

      for b holds (L /. b) = ( 1r * b)

      proof

        let b;

        b in COMPLEX by XCMPLX_0:def 2;

        hence thesis by A1, PARTFUN2: 6;

      end;

      then

      reconsider L as C_LinearFunc by Def4;

      now

        let h;

        now

          let n be Nat;

          

           A3: n in NAT & ( rng h) c= ( dom R) by ORDINAL1:def 12;

          

          thus (((h " ) (#) (R /* h)) . n) = (((h " ) . n) * ((R /* h) . n)) by VALUED_1: 5

          .= (((h " ) . n) * (R /. (h . n))) by A3, FUNCT_2: 109

          .= (((h " ) . n) * 0c )

          .= 0c ;

        end;

        then ((h " ) (#) (R /* h)) is constant & (((h " ) (#) (R /* h)) . 0 ) = 0c by VALUED_0:def 18;

        hence ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0c by CFCONT_1: 26, CFCONT_1: 27;

      end;

      then

      reconsider R as C_RestFunc by Def3;

      let f, Z;

      assume that

       A4: Z c= ( dom f) and

       A5: (f | Z) = ( id Z);

       A6:

      now

        let x be Complex;

        assume

         A7: x in Z;

        then ((f | Z) . x) = x by A5, FUNCT_1: 18;

        then (f . x) = x by A7, FUNCT_1: 49;

        hence (f /. x) = x by A4, A7, PARTFUN1:def 6;

      end;

       A8:

      now

        let x0;

        assume

         A9: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A10: N c= Z by Th9;

        

         A11: for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

        proof

          let x;

          

           A12: (x - x0) in COMPLEX by XCMPLX_0:def 2;

          assume x in N;

          

          hence ((f /. x) - (f /. x0)) = (x - (f /. x0)) by A6, A10

          .= (x - x0) by A6, A9

          .= ((L /. (x - x0)) + 0c ) by A1, PARTFUN2: 6, A12

          .= ((L /. (x - x0)) + (R /. (x - x0))) by FUNCOP_1: 7, A12;

        end;

        N c= ( dom f) by A4, A10;

        hence f is_differentiable_in x0 by A11;

      end;

      hence

       A13: f is_differentiable_on Z by A4, Th15;

      let x0;

      assume

       A14: x0 in Z;

      then

      consider N1 be Neighbourhood of x0 such that

       A15: N1 c= Z by Th9;

      

       A16: f is_differentiable_in x0 by A8, A14;

      then ex N be Neighbourhood of x0 st N c= ( dom f) & ex L, R st for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

      then

      consider N be Neighbourhood of x0 such that

       A17: N c= ( dom f);

      consider N2 be Neighbourhood of x0 such that

       A18: N2 c= N1 and

       A19: N2 c= N by Lm1;

      

       A20: N2 c= ( dom f) by A17, A19;

      

       A21: for x st x in N2 holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

      proof

        let x;

        

         A22: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        assume x in N2;

        then x in N1 by A18;

        

        hence ((f /. x) - (f /. x0)) = (x - (f /. x0)) by A6, A15

        .= (x - x0) by A6, A14

        .= ((L /. (x - x0)) + 0c ) by A1, PARTFUN2: 6, A22

        .= ((L /. (x - x0)) + (R /. (x - x0))) by FUNCOP_1: 7, A22;

      end;

      

      thus ((f `| Z) /. x0) = ( diff (f,x0)) by A13, A14, Def12

      .= (L /. 1r ) by A16, A20, A21, Def7

      .= 1r ;

    end;

    theorem :: CFDIFF_1:28

    for f1, f2, Z st Z c= ( dom (f1 + f2)) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds (f1 + f2) is_differentiable_on Z & for x st x in Z holds (((f1 + f2) `| Z) /. x) = (( diff (f1,x)) + ( diff (f2,x)))

    proof

      let f1, f2, Z;

      assume that

       A1: Z c= ( dom (f1 + f2)) and

       A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

        then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2, Th15;

        hence (f1 + f2) is_differentiable_in x0 by Th23;

      end;

      hence

       A3: (f1 + f2) is_differentiable_on Z by A1, Th15;

      now

        let x;

        assume

         A4: x in Z;

        then

         A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2, Th15;

        

        thus (((f1 + f2) `| Z) /. x) = ( diff ((f1 + f2),x)) by A3, A4, Def12

        .= (( diff (f1,x)) + ( diff (f2,x))) by A5, Th23;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:29

    for f1, f2, Z st Z c= ( dom (f1 - f2)) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds (f1 - f2) is_differentiable_on Z & for x st x in Z holds (((f1 - f2) `| Z) /. x) = (( diff (f1,x)) - ( diff (f2,x)))

    proof

      let f1, f2, Z;

      assume that

       A1: Z c= ( dom (f1 - f2)) and

       A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

        then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2, Th15;

        hence (f1 - f2) is_differentiable_in x0 by Th24;

      end;

      hence

       A3: (f1 - f2) is_differentiable_on Z by A1, Th15;

      now

        let x;

        assume

         A4: x in Z;

        then

         A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2, Th15;

        

        thus (((f1 - f2) `| Z) /. x) = ( diff ((f1 - f2),x)) by A3, A4, Def12

        .= (( diff (f1,x)) - ( diff (f2,x))) by A5, Th24;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:30

    for a, f, Z st Z c= ( dom (a (#) f)) & f is_differentiable_on Z holds (a (#) f) is_differentiable_on Z & for x st x in Z holds (((a (#) f) `| Z) /. x) = (a * ( diff (f,x)))

    proof

      let a, f, Z;

      assume that

       A1: Z c= ( dom (a (#) f)) and

       A2: f is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

        then f is_differentiable_in x0 by A2, Th15;

        hence (a (#) f) is_differentiable_in x0 by Th25;

      end;

      hence

       A3: (a (#) f) is_differentiable_on Z by A1, Th15;

      now

        let x;

        assume

         A4: x in Z;

        then

         A5: f is_differentiable_in x by A2, Th15;

        

        thus (((a (#) f) `| Z) /. x) = ( diff ((a (#) f),x)) by A3, A4, Def12

        .= (a * ( diff (f,x))) by A5, Th25;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:31

    for f1, f2, Z st Z c= ( dom (f1 (#) f2)) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds (f1 (#) f2) is_differentiable_on Z & for x st x in Z holds (((f1 (#) f2) `| Z) /. x) = (((f2 /. x) * ( diff (f1,x))) + ((f1 /. x) * ( diff (f2,x))))

    proof

      let f1, f2, Z;

      assume that

       A1: Z c= ( dom (f1 (#) f2)) and

       A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

        then f1 is_differentiable_in x0 & f2 is_differentiable_in x0 by A2, Th15;

        hence (f1 (#) f2) is_differentiable_in x0 by Th26;

      end;

      hence

       A3: (f1 (#) f2) is_differentiable_on Z by A1, Th15;

      now

        let x;

        assume

         A4: x in Z;

        then

         A5: f1 is_differentiable_in x & f2 is_differentiable_in x by A2, Th15;

        

        thus (((f1 (#) f2) `| Z) /. x) = ( diff ((f1 (#) f2),x)) by A3, A4, Def12

        .= (((f2 /. x) * ( diff (f1,x))) + ((f1 /. x) * ( diff (f2,x)))) by A5, Th26;

      end;

      hence thesis;

    end;

    theorem :: CFDIFF_1:32

    Z c= ( dom f) & (f | Z) is constant implies f is_differentiable_on Z & for x st x in Z holds ((f `| Z) /. x) = 0c

    proof

      reconsider cf = ( COMPLEX --> 0c ) as Function of COMPLEX , COMPLEX ;

      set R = cf;

      now

        let h;

        now

          let n be Nat;

          

           A2: n in NAT & ( rng h) c= ( dom R) by ORDINAL1:def 12;

          

          thus (((h " ) (#) (R /* h)) . n) = (((h " ) . n) * ((R /* h) . n)) by VALUED_1: 5

          .= (((h " ) . n) * (R /. (h . n))) by A2, FUNCT_2: 109

          .= (((h " ) . n) * 0c )

          .= 0c ;

        end;

        then ((h " ) (#) (R /* h)) is constant & (((h " ) (#) (R /* h)) . 0 ) = 0c by VALUED_0:def 18;

        hence ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0c by CFCONT_1: 26, CFCONT_1: 27;

      end;

      then

      reconsider R as C_RestFunc by Def3;

      set L = cf;

      for x holds (L /. x) = ( 0c * x) by XCMPLX_0:def 2, FUNCOP_1: 7;

      then

      reconsider L as C_LinearFunc by Def4;

      assume that

       A3: Z c= ( dom f) and

       A4: (f | Z) is constant;

      consider a1 be Element of COMPLEX such that

       A5: for x be Element of COMPLEX st x in (Z /\ ( dom f)) holds (f /. x) = a1 by A4, PARTFUN2: 35;

       A6:

      now

        let x0;

        assume

         A7: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A8: N c= Z by Th9;

        

         A9: N c= ( dom f) by A3, A8;

        

         A10: x0 in (Z /\ ( dom f)) by A3, A7, XBOOLE_0:def 4;

        for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

        proof

          let x;

          

           A11: (x - x0) in COMPLEX by XCMPLX_0:def 2;

          assume x in N;

          then x in (Z /\ ( dom f)) by A8, A9, XBOOLE_0:def 4;

          

          hence ((f /. x) - (f /. x0)) = (a1 - (f /. x0)) by A5

          .= (a1 - a1) by A5, A10

          .= ((L /. (x - x0)) + 0c ) by FUNCOP_1: 7, A11

          .= ((L /. (x - x0)) + (R /. (x - x0))) by FUNCOP_1: 7, A11;

        end;

        hence f is_differentiable_in x0 by A9;

      end;

      hence

       A12: f is_differentiable_on Z by A3, Th15;

      let x0;

      assume

       A13: x0 in Z;

      then

      consider N be Neighbourhood of x0 such that

       A14: N c= Z by Th9;

      

       A15: N c= ( dom f) by A3, A14;

      

       A16: x0 in (Z /\ ( dom f)) by A3, A13, XBOOLE_0:def 4;

      

       A17: for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

      proof

        let x;

        

         A18: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        assume x in N;

        then x in (Z /\ ( dom f)) by A14, A15, XBOOLE_0:def 4;

        

        hence ((f /. x) - (f /. x0)) = (a1 - (f /. x0)) by A5

        .= (a1 - a1) by A5, A16

        .= ((L /. (x - x0)) + 0c ) by FUNCOP_1: 7, A18

        .= ((L /. (x - x0)) + (R /. (x - x0))) by FUNCOP_1: 7, A18;

      end;

      

       A19: f is_differentiable_in x0 by A6, A13;

      

      thus ((f `| Z) /. x0) = ( diff (f,x0)) by A12, A13, Def12

      .= (L /. 1r ) by A19, A15, A17, Def7

      .= 0c ;

    end;

    theorem :: CFDIFF_1:33

    Z c= ( dom f) & (for x st x in Z holds (f /. x) = ((a * x) + b)) implies f is_differentiable_on Z & for x st x in Z holds ((f `| Z) /. x) = a

    proof

      reconsider cf = ( COMPLEX --> 0c ) as Function of COMPLEX , COMPLEX ;

      set R = cf;

      now

        let h;

        now

          let n be Nat;

          

           A2: n in NAT & ( rng h) c= ( dom R) by ORDINAL1:def 12;

          

          thus (((h " ) (#) (R /* h)) . n) = (((h " ) . n) * ((R /* h) . n)) by VALUED_1: 5

          .= (((h " ) . n) * (R /. (h . n))) by A2, FUNCT_2: 109

          .= (((h " ) . n) * 0c )

          .= 0c ;

        end;

        then ((h " ) (#) (R /* h)) is constant & (((h " ) (#) (R /* h)) . 0 ) = 0c by VALUED_0:def 18;

        hence ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0c by CFCONT_1: 26, CFCONT_1: 27;

      end;

      then

      reconsider R as C_RestFunc by Def3;

      assume that

       A3: Z c= ( dom f) and

       A4: for x st x in Z holds (f /. x) = ((a * x) + b);

      deffunc G( Complex) = ( In ((a * $1), COMPLEX ));

      consider L be Function of COMPLEX , COMPLEX such that

       A5: for x be Element of COMPLEX holds (L . x) = G(x) from FUNCT_2:sch 4;

      for z holds (L /. z) = (a * z)

      proof

        let z;

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

        (L . z) = G(z) by A5;

        hence thesis;

      end;

      then

      reconsider L as C_LinearFunc by Def4;

       A6:

      now

        let x0;

        assume

         A7: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A8: N c= Z by Th9;

        

         A9: for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

        proof

          let x;

          

           A10: (x - x0) in COMPLEX by XCMPLX_0:def 2;

          assume x in N;

          

          hence ((f /. x) - (f /. x0)) = (((a * x) + b) - (f /. x0)) by A4, A8

          .= (((a * x) + b) - ((a * x0) + b)) by A4, A7

          .= ( G(-) + 0c )

          .= ((L /. (x - x0)) + 0c ) by A5, A10

          .= ((L /. (x - x0)) + (R /. (x - x0))) by FUNCOP_1: 7, A10;

        end;

        N c= ( dom f) by A3, A8;

        hence f is_differentiable_in x0 by A9;

      end;

      hence

       A11: f is_differentiable_on Z by A3, Th15;

      let x0;

      assume

       A12: x0 in Z;

      then

      consider N be Neighbourhood of x0 such that

       A13: N c= Z by Th9;

      

       A14: for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)))

      proof

        let x;

        

         A15: (x - x0) in COMPLEX by XCMPLX_0:def 2;

        assume x in N;

        

        hence ((f /. x) - (f /. x0)) = (((a * x) + b) - (f /. x0)) by A4, A13

        .= (((a * x) + b) - ((a * x0) + b)) by A4, A12

        .= ( G(-) + 0c )

        .= ((L /. (x - x0)) + 0c ) by A5, A15

        .= ((L /. (x - x0)) + (R /. (x - x0))) by FUNCOP_1: 7, A15;

      end;

      

       A16: N c= ( dom f) by A3, A13;

      

       A17: f is_differentiable_in x0 by A6, A12;

      

      thus ((f `| Z) /. x0) = ( diff (f,x0)) by A11, A12, Def12

      .= (L /. 1r ) by A17, A16, A14, Def7

      .= G(1r) by A5

      .= a;

    end;

    theorem :: CFDIFF_1:34

    

     Th34: for x0 be Complex holds f is_differentiable_in x0 implies f is_continuous_in x0

    proof

      let x0 be Complex;

      assume

       A1: f is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

       A2: N c= ( dom f) and ex L, R st for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

      

       A3: x0 in N by Th7;

      now

        consider g be Real such that

         A4: 0 < g and

         A5: { y where y be Complex : |.(y - x0).| < g } c= N by Def5;

        reconsider xx0 = x0 as Element of COMPLEX by XCMPLX_0:def 2;

        reconsider s2 = ( NAT --> xx0) as Complex_Sequence;

        let s1 such that

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

         A7: s1 is convergent and

         A8: ( lim s1) = x0 and

         A9: for n holds (s1 . n) <> x0;

        consider l be Nat such that

         A10: for m be Nat st l <= m holds |.((s1 . m) - x0).| < g by A7, A8, A4, COMSEQ_2:def 6;

        

         A11: ( lim s2) = (s2 . 0 ) by CFCONT_1: 28

        .= x0;

        deffunc G( Nat) = ( In (((s1 . $1) - (s2 . $1)), COMPLEX ));

        consider s3 such that

         A12: for n be Element of NAT holds (s3 . n) = G(n) from FUNCT_2:sch 4;

        

         A13: for n holds (s3 . n) = ((s1 . n) - (s2 . n))

        proof

          let n;

          n in NAT by ORDINAL1:def 12;

          then (s3 . n) = G(n) by A12;

          hence thesis;

        end;

        

         A14: s3 = (s1 - s2) by A13, CFCONT_1: 1;

        

         A15: s2 is convergent by CFCONT_1: 26;

        then

         A16: s3 is convergent by A7, A14;

        ( lim s3) = ( lim (s1 - s2)) by A13, CFCONT_1: 1

        .= (x0 - x0) by A7, A8, A15, A11, COMSEQ_2: 26

        .= 0c ;

        then

         A17: ( lim (s3 ^\ l)) = 0c by A16, CFCONT_1: 21;

        reconsider c = (s2 ^\ l) as constant Complex_Sequence;

         A18:

        now

          given n be Element of NAT such that

           A19: (s3 . n) = 0c ;

          ((s1 . n) - (s2 . n)) = 0c by A13, A19;

          hence contradiction by A9;

        end;

         A20:

        now

          given n be Element of NAT such that

           A21: ((s3 ^\ l) . n) = 0c ;

          

           A22: (n + l) in NAT by ORDINAL1:def 12;

          (s3 . (n + l)) = 0c by A21, NAT_1:def 3;

          hence contradiction by A18, A22;

        end;

        then

         A23: (s3 ^\ l) is non-zero by COMSEQ_1: 4;

        (s3 ^\ l) is convergent by A16, CFCONT_1: 21;

        then

        reconsider h = (s3 ^\ l) as 0 -convergent non-zero Complex_Sequence by A17, A23, Def1;

        now

          let n be Element of NAT ;

          

          thus ((((f /* (h + c)) - (f /* c)) + (f /* c)) . n) = ((((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n)) by VALUED_1: 1

          .= ((((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n)) by CFCONT_1: 1

          .= ((f /* (h + c)) . n);

        end;

        then

         A24: (((f /* (h + c)) - (f /* c)) + (f /* c)) = (f /* (h + c));

        now

          let n be Element of NAT ;

          

           A25: (n + l) in NAT by ORDINAL1:def 12;

          

          thus ((h + c) . n) = ((((s1 - s2) + s2) ^\ l) . n) by A14, Th18

          .= (((s1 - s2) + s2) . (n + l)) by NAT_1:def 3

          .= (((s1 - s2) . (n + l)) + (s2 . (n + l))) by VALUED_1: 1, A25

          .= (((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l))) by CFCONT_1: 1

          .= ((s1 ^\ l) . n) by NAT_1:def 3;

        end;

        

        then

         A26: (((f /* (h + c)) - (f /* c)) + (f /* c)) = (f /* (s1 ^\ l)) by A24, FUNCT_2: 63

        .= ((f /* s1) ^\ l) by A6, VALUED_0: 27;

        

         A27: ( rng c) = {x0}

        proof

          thus ( rng c) c= {x0}

          proof

            let y be object;

            assume y in ( rng c);

            then

            consider n be Element of NAT such that

             A28: y = ((s2 ^\ l) . n) by FUNCT_2: 113;

            

             A29: (n + l) in NAT by ORDINAL1:def 12;

            y = (s2 . (n + l)) by A28, NAT_1:def 3;

            then y = x0 by FUNCOP_1: 7, A29;

            hence thesis by TARSKI:def 1;

          end;

          let y be object;

          assume y in {x0};

          then

           A30: y = x0 by TARSKI:def 1;

          

           A31: ( 0 + l) in NAT by ORDINAL1:def 12;

          (c . 0 ) = (s2 . ( 0 + l)) by NAT_1:def 3

          .= y by A30, FUNCOP_1: 7, A31;

          hence thesis by FUNCT_2: 4;

        end;

         A32:

        now

          let p be Real such that

           A33: 0 < p;

          reconsider n = 0 as Nat;

          take n;

          thus for m st n <= m holds |.(((f /* c) . m) - (f /. x0)).| < p

          proof

            let m such that n <= m;

            

             A34: (m + l) in NAT by ORDINAL1:def 12;

            

             A35: m in NAT by ORDINAL1:def 12;

             {x0} c= ( dom f) by A2, A3, ZFMISC_1: 31;

            

            then |.(((f /* c) . m) - (f /. x0)).| = |.((f /. (c . m)) - (f /. x0)).| by A27, FUNCT_2: 109, A35

            .= |.((f /. (s2 . (m + l))) - (f /. x0)).| by NAT_1:def 3

            .= |.((f /. x0) - (f /. x0)).| by FUNCOP_1: 7, A34

            .= 0 by ABSVALUE: 2;

            hence thesis by A33;

          end;

        end;

        then

         A36: (f /* c) is convergent;

        now

          let n be Element of NAT ;

          

           A37: (h . n) <> 0 by A20;

          

          thus ((h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) . n) = ((h . n) * (((h " ) (#) ((f /* (h + c)) - (f /* c))) . n)) by VALUED_1: 5

          .= ((h . n) * (((h " ) . n) * (((f /* (h + c)) - (f /* c)) . n))) by VALUED_1: 5

          .= ((h . n) * (((h . n) " ) * (((f /* (h + c)) - (f /* c)) . n))) by VALUED_1: 10

          .= (((h . n) * ((h . n) " )) * (((f /* (h + c)) - (f /* c)) . n))

          .= (1 * (((f /* (h + c)) - (f /* c)) . n)) by A37, XCMPLX_0:def 7

          .= (((f /* (h + c)) - (f /* c)) . n);

        end;

        then

         A38: (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ((f /* (h + c)) - (f /* c));

        ( rng (h + c)) c= N

        proof

          let y be object;

          assume

           A39: y in ( rng (h + c));

          then

          consider n be Element of NAT such that

           A40: y = ((h + c) . n) by FUNCT_2: 113;

          

           A41: (n + l) in NAT by ORDINAL1:def 12;

          reconsider y1 = y as Complex by A39;

          ((h + c) . n) = ((((s1 - s2) + s2) ^\ l) . n) by A14, Th18

          .= (((s1 - s2) + s2) . (n + l)) by NAT_1:def 3

          .= (((s1 - s2) . (n + l)) + (s2 . (n + l))) by VALUED_1: 1, A41

          .= (((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l))) by CFCONT_1: 1

          .= (s1 . (l + n));

          then |.(((h + c) . n) - x0).| < g by A10, NAT_1: 12;

          then y1 in { z where z be Complex : |.(z - x0).| < g } by A40;

          hence thesis by A5;

        end;

        then

         A42: ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A1, A2, A27, Th22;

        then

         A43: ((f /* (h + c)) - (f /* c)) is convergent by A38;

        then

         A44: (((f /* (h + c)) - (f /* c)) + (f /* c)) is convergent by A36;

        hence (f /* s1) is convergent by A26, CFCONT_1: 22;

        ( lim (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c))))) = ( 0c * ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))))) by A17, A42, COMSEQ_2: 30

        .= 0 ;

        

        then ( lim (((f /* (h + c)) - (f /* c)) + (f /* c))) = ( 0c + ( lim (f /* c))) by A38, A43, A36, COMSEQ_2: 14

        .= (f /. x0) by A32, A36, COMSEQ_2:def 6;

        hence (f /. x0) = ( lim (f /* s1)) by A44, A26, CFCONT_1: 23;

      end;

      hence thesis by A2, A3, CFCONT_1: 31;

    end;

    theorem :: CFDIFF_1:35

    f is_differentiable_on X implies f is_continuous_on X

    proof

      assume

       A1: f is_differentiable_on X;

      hence

       A2: X c= ( dom f);

      let x be Complex;

      assume x in X;

      then

       A3: x in ( dom (f | X)) by A2, RELAT_1: 57;

      (f | X) is differentiable by A1;

      then (f | X) is_differentiable_in x by A3;

      hence thesis by Th34;

    end;

    theorem :: CFDIFF_1:36

    f is_differentiable_on X & Z c= X implies f is_differentiable_on Z

    proof

      assume that

       A1: f is_differentiable_on X and

       A2: Z c= X;

      

       A3: (f | X) is differentiable by A1;

      X c= ( dom f) by A1;

      hence Z c= ( dom f) by A2;

      let x0;

      assume

       A4: x0 in ( dom (f | Z));

      then

       A5: x0 in ( dom f) by RELAT_1: 57;

      

       A6: x0 in Z by A4, RELAT_1: 57;

      then

      consider N1 be Neighbourhood of x0 such that

       A7: N1 c= Z by Th9;

      x0 in ( dom (f | X)) by A2, A5, A6, RELAT_1: 57;

      then (f | X) is_differentiable_in x0 by A3;

      then

      consider N be Neighbourhood of x0 such that

       A8: N c= ( dom (f | X)) and

       A9: ex L, R st for x st x in N holds (((f | X) /. x) - ((f | X) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

      consider N2 be Neighbourhood of x0 such that

       A10: N2 c= N and

       A11: N2 c= N1 by Lm1;

      

       A12: N2 c= Z by A7, A11;

      take N2;

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

      then ( dom (f | X)) c= ( dom f) by XBOOLE_1: 17;

      then N c= ( dom f) by A8;

      then N2 c= ( dom f) by A10;

      then N2 c= (( dom f) /\ Z) by A12, XBOOLE_1: 19;

      hence

       A13: N2 c= ( dom (f | Z)) by RELAT_1: 61;

      consider L, R such that

       A14: for x st x in N holds (((f | X) /. x) - ((f | X) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A9;

      take L, R;

      let x;

      assume

       A15: x in N2;

      then (((f | X) /. x) - ((f | X) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A10, A14;

      then

       A16: (((f | X) /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A2, A5, A6, PARTFUN2: 17;

      x in N by A10, A15;

      then ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A8, A16, PARTFUN2: 15;

      then ((f /. x) - ((f | Z) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A5, A6, PARTFUN2: 17;

      hence thesis by A13, A15, PARTFUN2: 15;

    end;

    ::$Canceled

    theorem :: CFDIFF_1:38

    f is_differentiable_in x0 implies ex R st (R /. 0c ) = 0c & R is_continuous_in 0c

    proof

      assume f is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that N c= ( dom f) and

       A1: ex L, R st for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0)));

      consider L, R such that

       A2: for x st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A1;

      take R;

      consider a such that

       A3: for z holds (L /. z) = (a * z) by Def4;

      ((f /. x0) - (f /. x0)) = ((L /. (x0 - x0)) + (R /. (x0 - x0))) by A2, Th7;

      then

       A4: 0c = ((a * 0c ) + (R /. 0c )) by A3;

      hence (R /. 0c ) = 0c ;

       A5:

      now

        let h;

        ((h " ) (#) (R /* h)) is bounded by Def3;

        then

        consider M be Real such that M > 0 and

         A6: for n holds |.(((h " ) (#) (R /* h)) . n).| < M by COMSEQ_2: 8;

        ( lim h) = 0 by Def1;

        then ( lim |.h.|) = |. 0 .| by SEQ_2: 27;

        

        then

         A7: ( lim (M (#) |.h.|)) = (M * |. 0 .|) by SEQ_2: 8

        .= (M * 0 ) by ABSVALUE: 2

        .= 0 ;

         A8:

        now

          let p be Real;

          assume 0 < p;

          then

          consider m such that

           A9: for n st m <= n holds |.(((M (#) |.h.|) . n) - 0 ).| < p by A7, SEQ_2:def 7;

          take m;

          now

            let n;

            assume m <= n;

            then

             A10: |.(((M (#) |.h.|) . n) - 0 ).| < p by A9;

             |.(((h " ) (#) (R /* h)) . n).| = |.(((h " ) . n) * ((R /* h) . n)).| by VALUED_1: 5

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

            then

             A11: |.(((h . n) " ) * ((R /* h) . n)).| <= M by A6;

            

             A12: n in NAT by ORDINAL1:def 12;

             |.(h . n).| >= 0 by COMPLEX1: 46;

            then ( |.(h . n).| * |.(((h . n) " ) * ((R /* h) . n)).|) <= (M * |.(h . n).|) by A11, XREAL_1: 64;

            then |.((h . n) * (((h . n) " ) * ((R /* h) . n))).| <= (M * |.(h . n).|) by COMPLEX1: 65;

            then (h . n) <> 0c & |.(((h . n) * ((h . n) " )) * ((R /* h) . n)).| <= (M * |.(h . n).|) by COMSEQ_1: 4, A12;

            then |.( 1r * ((R /* h) . n)).| <= (M * |.(h . n).|) by XCMPLX_0:def 7;

            then |.((R /* h) . n).| <= (M * ( |.h.| . n)) by VALUED_1: 18;

            then

             A13: |.((R /* h) . n).| <= ((M (#) |.h.|) . n) by SEQ_1: 9;

             0 <= |.((R /* h) . n).| by COMPLEX1: 46;

            then 0 <= ((M (#) |.h.|) . n) by A13;

            then ((M (#) |.h.|) . n) < p by A10, ABSVALUE:def 1;

            hence |.(((R /* h) . n) - 0c ).| < p by A13, XXREAL_0: 2;

          end;

          hence for n st m <= n holds |.(((R /* h) . n) - 0c ).| < p;

        end;

        hence (R /* h) is convergent;

        hence ( lim (R /* h)) = (R /. 0c ) by A4, A8, COMSEQ_2:def 6;

      end;

       A14:

      now

        let s1;

        assume that ( rng s1) c= ( dom R) and

         A15: s1 is convergent & ( lim s1) = 0 and

         A16: for n holds (s1 . n) <> 0 ;

        for n be Element of NAT holds (s1 . n) <> 0 by A16;

        then s1 is non-zero by COMSEQ_1: 4;

        then s1 is 0 -convergent non-zero Complex_Sequence by A15, Def1;

        hence (R /* s1) is convergent & ( lim (R /* s1)) = (R /. 0c ) by A5;

      end;

      ( dom R) = COMPLEX by PARTFUN1:def 2;

      hence thesis by A14, CFCONT_1: 31;

    end;