cfdiff_2.miz



    begin

    reserve n,m for Element of NAT ;

    reserve z for Complex;

    

     Lm1: for seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real st seq = cseq & seq is convergent & ( lim seq) = rlim holds ( lim cseq) = rlim

    proof

      let seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real such that

       A1: seq = cseq & seq is convergent & ( lim seq) = rlim;

      reconsider clim = rlim as Element of COMPLEX by XCMPLX_0:def 2;

      cseq is convergent & for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((cseq . m) - clim).| < p by A1, SEQ_2:def 7;

      hence thesis by COMSEQ_2:def 6;

    end;

    

     Lm2: for seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real st seq = cseq & cseq is convergent & ( lim cseq) = rlim holds ( lim seq) = rlim

    proof

      let seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real such that

       A1: seq = cseq and

       A2: cseq is convergent and

       A3: ( lim cseq) = rlim;

      reconsider clim = rlim as Complex;

      

       A4: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((seq . m) - rlim).| < p by A1, A2, A3, COMSEQ_2:def 6;

      seq is convergent by A1, A2;

      hence ( lim seq) = rlim by A4, SEQ_2:def 7;

    end;

    

     Lm3: for seq be Real_Sequence, cseq be Complex_Sequence st seq = cseq holds seq is 0 -convergent non-zero iff cseq is 0 -convergent non-zero

    proof

      let seq be Real_Sequence, cseq be Complex_Sequence such that

       A1: seq = cseq;

      thus seq is 0 -convergent non-zero implies cseq is 0 -convergent non-zero

      proof

        assume

         A2: seq is 0 -convergent non-zero;

        then

         A3: seq is convergent;

        ( lim seq) = 0 by A2;

        then

         A4: ( lim cseq) = 0 by A1, A3, Lm1;

        

         A5: cseq is non-zero by A1, A2;

        cseq is convergent by A1, A3;

        hence cseq is 0 -convergent non-zero by A5, A4, CFDIFF_1:def 1;

      end;

      assume

       A6: cseq is 0 -convergent non-zero;

      then ( lim cseq) = 0 by CFDIFF_1:def 1;

      then

       A7: ( lim seq) = 0 by A1, A6, Lm2;

      thus seq is 0 -convergent non-zero by A1, A6, A7, FDIFF_1:def 1;

    end;

    theorem :: CFDIFF_2:1

    

     Th1: for f be PartFunc of COMPLEX , COMPLEX st f is total holds ( dom ( Re f)) = COMPLEX & ( dom ( Im f)) = COMPLEX

    proof

      let f be PartFunc of COMPLEX , COMPLEX ;

      assume f is total;

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

      hence thesis by COMSEQ_3:def 3, COMSEQ_3:def 4;

    end;

    

     Lm4: for seq,cseq be Complex_Sequence st cseq = ( <i> (#) seq) holds seq is non-zero iff cseq is non-zero

    proof

      let seq,cseq be Complex_Sequence such that

       A1: cseq = ( <i> (#) seq);

      thus seq is non-zero implies cseq is non-zero by A1, COMSEQ_1: 38;

      

       A2: ( <i> (#) seq) is non-zero implies seq is non-zero

      proof

        assume

         A3: ( <i> (#) seq) is non-zero;

        now

          let n;

          (( <i> (#) seq) . n) <> 0c by A3, COMSEQ_1: 4;

          then ( <i> * (seq . n)) <> 0c by VALUED_1: 6;

          hence (seq . n) <> 0c ;

        end;

        hence thesis by COMSEQ_1: 4;

      end;

      assume cseq is non-zero;

      hence seq is non-zero by A1, A2;

    end;

    

     Lm5: for seq,cseq be Complex_Sequence st cseq = ( <i> (#) seq) holds seq is 0 -convergent non-zero iff cseq is 0 -convergent non-zero

    proof

      let seq,cseq be Complex_Sequence such that

       A1: cseq = ( <i> (#) seq);

      thus seq is 0 -convergent non-zero implies cseq is 0 -convergent non-zero

      proof

        assume

         A2: seq is 0 -convergent non-zero;

        then ( lim seq) = 0 by CFDIFF_1:def 1;

        

        then

         A3: ( lim ( <i> (#) seq)) = ( <i> * 0 ) by A2, COMSEQ_2: 18

        .= 0 ;

        ( <i> (#) seq) is non-zero & ( <i> (#) seq) is convergent by A2, COMSEQ_1: 38;

        hence cseq is 0 -convergent non-zero by A1, A3, CFDIFF_1:def 1;

      end;

      assume

       A4: cseq is 0 -convergent non-zero;

      then

       A5: seq is non-zero by A1, Lm4;

      (( - <i> ) (#) ( <i> (#) seq)) is convergent by A1, A4;

      then ((( - <i> ) * <i> ) (#) seq) is convergent by CFUNCT_1: 22;

      then

       A6: seq is convergent by CFUNCT_1: 26;

      ( lim ( <i> (#) seq)) = 0 by A1, A4, CFDIFF_1:def 1;

      then ( <i> * ( lim seq)) = 0 by A6, COMSEQ_2: 18;

      hence seq is 0 -convergent non-zero by A6, A5, CFDIFF_1:def 1;

    end;

    theorem :: CFDIFF_2:2

    

     Th2: for f be PartFunc of COMPLEX , COMPLEX , u,v be PartFunc of ( REAL 2), REAL , z0 be Complex, x0,y0 be Real, xy0 be Element of ( REAL 2) st (for x,y be Real st (x + (y * <i> )) in ( dom f) holds <*x, y*> in ( dom u) & (u . <*x, y*>) = (( Re f) . (x + (y * <i> )))) & (for x,y be Real st (x + (y * <i> )) in ( dom f) holds <*x, y*> in ( dom v) & (v . <*x, y*>) = (( Im f) . (x + (y * <i> )))) & z0 = (x0 + (y0 * <i> )) & xy0 = <*x0, y0*> & f is_differentiable_in z0 holds u is_partial_differentiable_in (xy0,1) & u is_partial_differentiable_in (xy0,2) & v is_partial_differentiable_in (xy0,1) & v is_partial_differentiable_in (xy0,2) & ( Re ( diff (f,z0))) = ( partdiff (u,xy0,1)) & ( Re ( diff (f,z0))) = ( partdiff (v,xy0,2)) & ( Im ( diff (f,z0))) = ( - ( partdiff (u,xy0,2))) & ( Im ( diff (f,z0))) = ( partdiff (v,xy0,1))

    proof

      let f be PartFunc of COMPLEX , COMPLEX , u,v be PartFunc of ( REAL 2), REAL , z0 be Complex, x00,y00 be Real, xy0 be Element of ( REAL 2) such that

       A1: for x,y be Real st (x + (y * <i> )) in ( dom f) holds <*x, y*> in ( dom u) & (u . <*x, y*>) = (( Re f) . (x + (y * <i> ))) and

       A2: for x,y be Real st (x + (y * <i> )) in ( dom f) holds <*x, y*> in ( dom v) & (v . <*x, y*>) = (( Im f) . (x + (y * <i> ))) and

       A3: z0 = (x00 + (y00 * <i> )) and

       A4: xy0 = <*x00, y00*> and

       A5: f is_differentiable_in z0;

      reconsider x0 = x00, y0 = y00 as Element of REAL by XREAL_0:def 1;

      

       A6: z0 = (x0 + (y0 * <i> )) by A3;

      

       A7: xy0 = <*x0, y0*> by A4;

      deffunc LDF2( Real) = ( In ((( Im ( diff (f,z0))) * $1), REAL ));

      consider LD2 be Function of REAL , REAL such that

       A8: for x be Element of REAL holds (LD2 . x) = LDF2(x) from FUNCT_2:sch 4;

      

       A9: for x be Real holds (LD2 . x) = (( Im ( diff (f,z0))) * x)

      proof

        let x be Real;

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

        (LD2 . x) = LDF2(x) by A8;

        hence thesis;

      end;

      reconsider LD2 as LinearFunc by A9, FDIFF_1:def 3;

      deffunc LDF1( Real) = ( In ((( Re ( diff (f,z0))) * $1), REAL ));

      consider LD1 be Function of REAL , REAL such that

       A10: for x be Element of REAL holds (LD1 . x) = LDF1(x) from FUNCT_2:sch 4;

      

       A11: for x be Real holds (LD1 . x) = (( Re ( diff (f,z0))) * x)

      proof

        let x be Real;

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

        (LD1 . x) = LDF1(x) by A10;

        hence thesis;

      end;

      

       A12: for y be Real holds ((v * ( reproj (2,xy0))) . y) = (v . <*x0, y*>)

      proof

        let y be Real;

        reconsider yy = y, dwa = 2 as Element of REAL by XREAL_0:def 1;

        yy in REAL ;

        then yy in ( dom ( reproj (2,xy0))) by PDIFF_1:def 5;

        

        hence ((v * ( reproj (2,xy0))) . y) = (v . (( reproj (2,xy0)) . y)) by FUNCT_1: 13

        .= (v . ( Replace (xy0,2,yy))) by PDIFF_1:def 5

        .= (v . <*x0, yy*>) by A7, FINSEQ_7: 14

        .= (v . <*x0, y*>);

      end;

      

       A13: for y be Real holds ((u * ( reproj (2,xy0))) . y) = (u . <*x0, y*>)

      proof

        let y be Real;

        reconsider yy = y as Element of REAL by XREAL_0:def 1;

        y in REAL by XREAL_0:def 1;

        then y in ( dom ( reproj (2,xy0))) by PDIFF_1:def 5;

        

        hence ((u * ( reproj (2,xy0))) . y) = (u . (( reproj (2,xy0)) . y)) by FUNCT_1: 13

        .= (u . ( Replace (xy0,2,yy))) by PDIFF_1:def 5

        .= (u . <*x0, y*>) by A7, FINSEQ_7: 14;

      end;

      

       A14: (( proj (2,2)) . xy0) = (xy0 . 2) by PDIFF_1:def 1

      .= y0 by A7, FINSEQ_1: 44;

      reconsider LD1 as LinearFunc by A11, FDIFF_1:def 3;

      deffunc LDF3( Real) = ( In (( - (( Im ( diff (f,z0))) * $1)), REAL ));

      consider LD3 be Function of REAL , REAL such that

       A15: for x be Element of REAL holds (LD3 . x) = LDF3(x) from FUNCT_2:sch 4;

      

       A16: for x be Real holds (LD3 . x) = ( - (( Im ( diff (f,z0))) * x))

      proof

        let x be Real;

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

        (LD3 . x) = LDF3(x) by A15;

        hence thesis;

      end;

      for x be Real holds (LD3 . x) = (( - ( Im ( diff (f,z0)))) * x)

      proof

        let x be Real;

        

        thus (LD3 . x) = ( - (( Im ( diff (f,z0))) * x)) by A16

        .= (( - ( Im ( diff (f,z0)))) * x);

      end;

      then

      reconsider LD3 as LinearFunc by FDIFF_1:def 3;

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

      consider N be Neighbourhood of z0 such that

       A17: N c= ( dom f) and

       A18: ex L be C_LinearFunc, R be C_RestFunc st ( diff (f,z0)) = (L /. 1r ) & for z be Complex st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) by A5, CFDIFF_1:def 7;

      consider L be C_LinearFunc, R be C_RestFunc such that

       A19: ( diff (f,z0)) = (L /. 1r ) & for z be Complex st z in N holds ((f /. z) - (f /. z0)) = ((L /. (z - z0)) + (R /. (z - z0))) by A18;

      deffunc RF4( Real) = ( In ((( Im R) . ($1 * <i> )), REAL ));

      consider R4 be Function of REAL , REAL such that

       A20: for y be Element of REAL holds (R4 . y) = RF4(y) from FUNCT_2:sch 4;

      

       A21: for z be Complex st z in N holds ((f /. z) - (f /. z0)) = ((( diff (f,z0)) * (z - z0)) + (R /. (z - z0)))

      proof

        let z be Complex;

        assume

         A22: z in N;

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

        consider a0 be Complex such that

         A23: for w be Complex holds (L /. w) = (a0 * w) by CFDIFF_1:def 4;

        (L /. ( 1r * (z - z0))) = ((a0 * 1r ) * (z - z0)) by A23

        .= ((L /. 1r ) * (z - z0)) by A23;

        hence thesis by A19, A22;

      end;

      

       A24: for x,y be Real st (x + (y * <i> )) in N & (x0 + (y0 * <i> )) in N holds ((f . (x + (y * <i> ))) - (f . (x0 + (y0 * <i> )))) = ((( diff (f,z0)) * ((x + (y * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x + (y * <i> )) - (x0 + (y0 * <i> )))))

      proof

        let x,y be Real;

        assume

         A25: (x + (y * <i> )) in N & (x0 + (y0 * <i> )) in N;

        then (f . (x + (y * <i> ))) = (f /. (x + (y * <i> ))) & (f . (x0 + (y0 * <i> ))) = (f /. (x0 + (y0 * <i> ))) by A17, PARTFUN1:def 6;

        hence thesis by A21, A25, A6;

      end;

      

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

      for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R4 /* h)) is convergent & ( lim ((h " ) (#) (R4 /* h))) = 0

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        ( rng h) c= COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

        then

        reconsider hz0 = h as Complex_Sequence by FUNCT_2: 6;

        reconsider hz0 as 0 -convergent non-zero Complex_Sequence by Lm3;

        set hz = ( <i> (#) hz0);

        reconsider hz as 0 -convergent non-zero Complex_Sequence by Lm5;

        now

          

           A27: ( rng hz) c= ( dom R) by A26;

          ( dom R4) = REAL by PARTFUN1:def 2;

          then

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

          let n be Nat;

          

           A29: n in NAT by ORDINAL1:def 12;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          

           A30: ( Im ((h . nn) " )) = 0 & ( Re ((h . nn) " )) = ((h . nn) " ) by COMPLEX1:def 1, COMPLEX1:def 2;

          

           A31: (hz . n) = ((h . n) * <i> ) by VALUED_1: 6;

          reconsider hn = (h . n) as Real;

          ((h . n) * <i> ) in COMPLEX by XCMPLX_0:def 2;

          then

           A32: ((h . n) * <i> ) in ( dom ( Im R)) by Th1;

          

          thus (((h " ) (#) (R4 /* h)) . n) = (((h " ) . n) * ((R4 /* h) . n)) by SEQ_1: 8

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

          .= (((h . n) " ) * (R4 . hn)) by A28, FUNCT_2: 108, A29

          .= (((h . nn) " ) * RF4(hn)) by A20

          .= (((h . n) " ) * (( Im R) . ((h . n) * <i> )))

          .= ((( Re ((h . n) " )) * ( Im (R . ((h . n) * <i> )))) + (( Re (R . ((h . n) * <i> ))) * ( Im ((h . n) " )))) by A32, A30, COMSEQ_3:def 4

          .= ( Im ((((hz . n) / <i> ) " ) * (R . (hz . n)))) by A31, COMPLEX1: 9

          .= ( Im (( <i> / (hz . n)) * (R . (hz . n)))) by XCMPLX_1: 213

          .= ( Im (( <i> * ((hz " ) . n)) * (R . (hz . n)))) by VALUED_1: 10

          .= ( Im ( <i> * (((hz " ) . n) * (R . (hz . n)))))

          .= ((( Re <i> ) * ( Im (((hz " ) . n) * (R /. (hz . n))))) + (( Re (((hz " ) . n) * (R /. (hz . n)))) * ( Im <i> ))) by COMPLEX1: 9

          .= ( Re (((hz " ) . n) * ((R /* hz) . n))) by A27, COMPLEX1: 7, FUNCT_2: 109, A29

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

        end;

        then

         A33: ((h " ) (#) (R4 /* h)) = ( Re ((hz " ) (#) (R /* hz))) by COMSEQ_3:def 5;

        ((hz " ) (#) (R /* hz)) is convergent & ( lim ((hz " ) (#) (R /* hz))) = 0 by CFDIFF_1:def 3;

        hence thesis by A33, COMPLEX1: 4, COMSEQ_3: 41;

      end;

      then

      reconsider R4 as RestFunc by FDIFF_1:def 2;

      deffunc RF2( Real) = ( In ((( Re R) . ($1 * <i> )), REAL ));

      

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

      consider R2 be Function of REAL , REAL such that

       A35: for y be Element of REAL holds (R2 . y) = RF2(y) from FUNCT_2:sch 4;

      for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R2 /* h)) is convergent & ( lim ((h " ) (#) (R2 /* h))) = 0

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        ( rng h) c= COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

        then

        reconsider hz0 = h as Complex_Sequence by FUNCT_2: 6;

        reconsider hz0 as 0 -convergent non-zero Complex_Sequence by Lm3;

        set hz = ( <i> (#) hz0);

        reconsider hz as 0 -convergent non-zero Complex_Sequence by Lm5;

        

         A36: ((hz " ) (#) (R /* hz)) is convergent by CFDIFF_1:def 3;

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

        then

         A37: ( rng hz) c= ( dom R);

        now

          ( dom R2) = REAL by PARTFUN1:def 2;

          then

           A38: ( rng h) c= ( dom R2);

          let n be Nat;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          

           A39: ( Im ((h . nn) " )) = 0 & ( Re ((h . nn) " )) = ((h . nn) " ) by COMPLEX1:def 1, COMPLEX1:def 2;

          

           A40: (hz . n) = ((h . n) * <i> ) by VALUED_1: 6;

          ( dom ( Re R)) = COMPLEX by Th1;

          then

           A41: ((h . n) * <i> ) in ( dom ( Re R)) by XCMPLX_0:def 2;

          

           A42: (R . (hz . n)) = (R /. (hz . n));

          reconsider hn = (h . n) as Real;

          

          thus (((h " ) (#) (R2 /* h)) . n) = (((h " ) . n) * ((R2 /* h) . n)) by SEQ_1: 8

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

          .= (((h . nn) " ) * (R2 . (h . n))) by A38, FUNCT_2: 108

          .= (((h . nn) " ) * RF2(hn)) by A35

          .= (((h . n) " ) * (( Re R) . ((h . n) * <i> )))

          .= ((( Re ((h . n) " )) * ( Re (R . ((h . n) * <i> )))) - (( Im ((h . n) " )) * ( Im (R . ((h . n) * <i> ))))) by A41, A39, COMSEQ_3:def 3

          .= ( Re ((((hz . n) / <i> ) " ) * (R . (hz . n)))) by A40, COMPLEX1: 9

          .= ( Re (( <i> / (hz . n)) * (R . (hz . n)))) by XCMPLX_1: 213

          .= ( Re (( <i> * ((hz " ) . n)) * (R . (hz . n)))) by VALUED_1: 10

          .= ( Re ( <i> * (((hz " ) . n) * (R . (hz . n)))))

          .= ((( Re <i> ) * ( Re (((hz " ) . n) * (R . (hz . n))))) - (( Im <i> ) * ( Im (((hz " ) . n) * (R . (hz . n)))))) by COMPLEX1: 9

          .= ( - ( Im (((hz " ) . nn) * ((R /* hz) . nn)))) by A42, A37, COMPLEX1: 7, FUNCT_2: 109

          .= ( - ( Im (((hz " ) (#) (R /* hz)) . n))) by VALUED_1: 5

          .= ( - (( Im ((hz " ) (#) (R /* hz))) . n)) by COMSEQ_3:def 6;

        end;

        then

         A43: ((h " ) (#) (R2 /* h)) = ( - ( Im ((hz " ) (#) (R /* hz)))) by SEQ_1: 10;

        ( lim ((hz " ) (#) (R /* hz))) = 0 by CFDIFF_1:def 3;

        then ( lim ( Im ((hz " ) (#) (R /* hz)))) = ( Im 0 ) by A36, COMSEQ_3: 41;

        

        then ( lim ((h " ) (#) (R2 /* h))) = ( - ( Im 0 )) by A43, A36, SEQ_2: 10

        .= 0 by COMPLEX1: 4;

        hence thesis by A43, A36, SEQ_2: 9;

      end;

      then

      reconsider R2 as RestFunc by FDIFF_1:def 2;

      consider r0 be Real such that

       A44: 0 < r0 and

       A45: { y where y be Complex : |.(y - z0).| < r0 } c= N by CFDIFF_1:def 5;

      set Ny0 = ].(y0 - r0), (y0 + r0).[;

      reconsider Ny0 as Neighbourhood of y0 by A44, RCOMP_1:def 6;

      

       A46: for y be Real st y in Ny0 holds (x0 + (y * <i> )) in N

      proof

        let y be Real;

         |.((x0 + (y * <i> )) - z0).| = |.((y - y0) * <i> ).| by A6;

        then

         A47: |.((x0 + (y * <i> )) - z0).| = ( |.(y - y0).| * |. <i> .|) by COMPLEX1: 65;

        assume y in Ny0;

        then (x0 + (y * <i> )) is Complex & |.((x0 + (y * <i> )) - z0).| < r0 by A47, COMPLEX1: 49, RCOMP_1: 1;

        then (x0 + (y * <i> )) in { w where w be Complex : |.(w - z0).| < r0 };

        hence (x0 + (y * <i> )) in N by A45;

      end;

      

       A48: for x,y be Real holds (( diff (f,z0)) * ((x + (y * <i> )) - (x0 + (y0 * <i> )))) = (((( Re ( diff (f,z0))) * (x - x0)) - (( Im ( diff (f,z0))) * (y - y0))) + (((( Im ( diff (f,z0))) * (x - x0)) + (( Re ( diff (f,z0))) * (y - y0))) * <i> ))

      proof

        let x,y be Real;

        

        thus (( diff (f,z0)) * ((x + (y * <i> )) - (x0 + (y0 * <i> )))) = ((( Re ( diff (f,z0))) + (( Im ( diff (f,z0))) * <i> )) * ((x - x0) + ((y - y0) * <i> ))) by COMPLEX1: 13

        .= (((( Re ( diff (f,z0))) * (x - x0)) - (( Im ( diff (f,z0))) * (y - y0))) + (((( Im ( diff (f,z0))) * (x - x0)) + (( Re ( diff (f,z0))) * (y - y0))) * <i> ));

      end;

      

       A49: for x,y be Real holds ( Re (( diff (f,z0)) * ((x + (y * <i> )) - (x0 + (y0 * <i> ))))) = ((( Re ( diff (f,z0))) * (x - x0)) - (( Im ( diff (f,z0))) * (y - y0)))

      proof

        let x,y be Real;

        

        thus ( Re (( diff (f,z0)) * ((x + (y * <i> )) - (x0 + (y0 * <i> ))))) = ( Re (((( Re ( diff (f,z0))) * (x - x0)) - (( Im ( diff (f,z0))) * (y - y0))) + (((( Im ( diff (f,z0))) * (x - x0)) + (( Re ( diff (f,z0))) * (y - y0))) * <i> ))) by A48

        .= ((( Re ( diff (f,z0))) * (x - x0)) - (( Im ( diff (f,z0))) * (y - y0))) by COMPLEX1: 12;

      end;

      

       A50: for y be Real st y in Ny0 holds ((u . <*x0, y*>) - (u . <*x0, y0*>)) = (( - (( Im ( diff (f,z0))) * (y - y0))) + (( Re R) . ((x0 - x0) + ((y - y0) * <i> ))))

      proof

        let y be Real;

        ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))) in ( dom R) by A34, XCMPLX_0:def 2;

        then

         A51: ((y - y0) * <i> ) in ( dom ( Re R)) by COMSEQ_3:def 3;

        assume y in Ny0;

        then

         A52: (x0 + (y * <i> )) in N by A46;

        then (x0 + (y * <i> )) in ( dom f) by A17;

        then

         A53: (x0 + (y * <i> )) in ( dom ( Re f)) by COMSEQ_3:def 3;

        

         A54: (x0 + (y0 * <i> )) in N by A6, CFDIFF_1: 7;

        then (x0 + (y0 * <i> )) in ( dom f) by A17;

        then

         A55: (x0 + (y0 * <i> )) in ( dom ( Re f)) by COMSEQ_3:def 3;

        ((u . <*x0, y*>) - (u . <*x0, y0*>)) = ((( Re f) . (x0 + (y * <i> ))) - (u . <*x0, y0*>)) by A1, A17, A52

        .= ((( Re f) . (x0 + (y * <i> ))) - (( Re f) . (x0 + (y0 * <i> )))) by A1, A17, A54

        .= (( Re (f . (x0 + (y * <i> )))) - (( Re f) . (x0 + (y0 * <i> )))) by A53, COMSEQ_3:def 3

        .= (( Re (f . (x0 + (y * <i> )))) - ( Re (f . (x0 + (y0 * <i> ))))) by A55, COMSEQ_3:def 3

        .= ( Re ((f . (x0 + (y * <i> ))) - (f . (x0 + (y0 * <i> ))))) by COMPLEX1: 19

        .= ( Re ((( diff (f,z0)) * ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))))) by A24, A52, A54

        .= (( Re (( diff (f,z0)) * ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) + ( Re (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))))) by COMPLEX1: 8

        .= (((( Re ( diff (f,z0))) * (x0 - x0)) - (( Im ( diff (f,z0))) * (y - y0))) + ( Re (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))))) by A49

        .= (((( Re ( diff (f,z0))) * 0 ) - (( Im ( diff (f,z0))) * (y - y0))) + ( Re (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))))

        .= (( - (( Im ( diff (f,z0))) * (y - y0))) + ( Re (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))))

        .= (( - (( Im ( diff (f,z0))) * (y - y0))) + ( Re (R . ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))))

        .= (( - (( Im ( diff (f,z0))) * (y - y0))) + (( Re R) . ((x0 - x0) + ((y - y0) * <i> )))) by A51, COMSEQ_3:def 3;

        hence thesis;

      end;

      

       A56: for y be Real st y in Ny0 holds (((u * ( reproj (2,xy0))) . y) - ((u * ( reproj (2,xy0))) . y0)) = ((LD3 . (y - y0)) + (R2 . (y - y0)))

      proof

        let y be Real;

        assume

         A57: y in Ny0;

        reconsider yy0 = (y - y0) as Element of REAL by XREAL_0:def 1;

        

        thus (((u * ( reproj (2,xy0))) . y) - ((u * ( reproj (2,xy0))) . y0)) = ((u . <*x0, y*>) - ((u * ( reproj (2,xy0))) . y0)) by A13

        .= ((u . <*x0, y*>) - (u . <*x0, y0*>)) by A13

        .= (( - (( Im ( diff (f,z0))) * (y - y0))) + (( Re R) . ((x0 - x0) + ((y - y0) * <i> )))) by A50, A57

        .= ((LD3 . (y - y0)) + (( Re R) . ((x0 - x0) + ((y - y0) * <i> )))) by A16

        .= ((LD3 . (y - y0)) + RF2(yy0))

        .= ((LD3 . (y - y0)) + (R2 . (y - y0))) by A35;

      end;

      

       A58: for x,y be Real holds ( Im (( diff (f,z0)) * ((x + (y * <i> )) - (x0 + (y0 * <i> ))))) = ((( Im ( diff (f,z0))) * (x - x0)) + (( Re ( diff (f,z0))) * (y - y0)))

      proof

        let x,y be Real;

        

        thus ( Im (( diff (f,z0)) * ((x + (y * <i> )) - (x0 + (y0 * <i> ))))) = ( Im (((( Re ( diff (f,z0))) * (x - x0)) - (( Im ( diff (f,z0))) * (y - y0))) + (((( Im ( diff (f,z0))) * (x - x0)) + (( Re ( diff (f,z0))) * (y - y0))) * <i> ))) by A48

        .= ((( Im ( diff (f,z0))) * (x - x0)) + (( Re ( diff (f,z0))) * (y - y0))) by COMPLEX1: 12;

      end;

      

       A59: for y be Real st y in Ny0 holds ((v . <*x0, y*>) - (v . <*x0, y0*>)) = ((( Re ( diff (f,z0))) * (y - y0)) + (( Im R) . ((x0 - x0) + ((y - y0) * <i> ))))

      proof

        let y be Real;

        ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))) in ( dom R) by A34, XCMPLX_0:def 2;

        then

         A60: ((y - y0) * <i> ) in ( dom ( Im R)) by COMSEQ_3:def 4;

        assume y in Ny0;

        then

         A61: (x0 + (y * <i> )) in N by A46;

        then (x0 + (y * <i> )) in ( dom f) by A17;

        then

         A62: (x0 + (y * <i> )) in ( dom ( Im f)) by COMSEQ_3:def 4;

        

         A63: (x0 + (y0 * <i> )) in N by A6, CFDIFF_1: 7;

        then (x0 + (y0 * <i> )) in ( dom f) by A17;

        then

         A64: (x0 + (y0 * <i> )) in ( dom ( Im f)) by COMSEQ_3:def 4;

        ((v . <*x0, y*>) - (v . <*x0, y0*>)) = ((( Im f) . (x0 + (y * <i> ))) - (v . <*x0, y0*>)) by A2, A17, A61

        .= ((( Im f) . (x0 + (y * <i> ))) - (( Im f) . (x0 + (y0 * <i> )))) by A2, A17, A63

        .= (( Im (f . (x0 + (y * <i> )))) - (( Im f) . (x0 + (y0 * <i> )))) by A62, COMSEQ_3:def 4

        .= (( Im (f . (x0 + (y * <i> )))) - ( Im (f . (x0 + (y0 * <i> ))))) by A64, COMSEQ_3:def 4

        .= ( Im ((f . (x0 + (y * <i> ))) - (f . (x0 + (y0 * <i> ))))) by COMPLEX1: 19

        .= ( Im ((( diff (f,z0)) * ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))))) by A24, A61, A63

        .= (( Im (( diff (f,z0)) * ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) + ( Im (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))))) by COMPLEX1: 8

        .= (((( Im ( diff (f,z0))) * (x0 - x0)) + (( Re ( diff (f,z0))) * (y - y0))) + ( Im (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))))) by A58

        .= (((( Im ( diff (f,z0))) * (x0 - x0)) + (( Re ( diff (f,z0))) * (y - y0))) + ( Im (R . ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))))

        .= ((( Re ( diff (f,z0))) * (y - y0)) + (( Im R) . ((x0 - x0) + ((y - y0) * <i> )))) by A60, COMSEQ_3:def 4;

        hence thesis;

      end;

      

       A65: for y be Real st y in Ny0 holds (((v * ( reproj (2,xy0))) . y) - ((v * ( reproj (2,xy0))) . y0)) = ((LD1 . (y - y0)) + (R4 . (y - y0)))

      proof

        let y be Real;

        assume

         A66: y in Ny0;

        reconsider yy0 = (y - y0) as Element of REAL by XREAL_0:def 1;

        

        thus (((v * ( reproj (2,xy0))) . y) - ((v * ( reproj (2,xy0))) . y0)) = ((v . <*x0, y*>) - ((v * ( reproj (2,xy0))) . y0)) by A12

        .= ((v . <*x0, y*>) - (v . <*x0, y0*>)) by A12

        .= ((( Re ( diff (f,z0))) * (y - y0)) + (( Im R) . ((x0 - x0) + ((y - y0) * <i> )))) by A59, A66

        .= ((LD1 . (y - y0)) + (( Im R) . ((x0 - x0) + ((y - y0) * <i> )))) by A11

        .= ((LD1 . (y - y0)) + RF4(yy0))

        .= ((LD1 . (y - y0)) + (R4 . (y - y0))) by A20;

      end;

      now

        let s be object;

        assume s in (( reproj (2,xy0)) .: Ny0);

        then

        consider y be Element of REAL such that

         A67: y in Ny0 and

         A68: s = (( reproj (2,xy0)) . y) by FUNCT_2: 65;

        

         A69: (x0 + (y * <i> )) in N by A46, A67;

        s = ( Replace (xy0,2,y)) by A68, PDIFF_1:def 5

        .= <*x0, y*> by A7, FINSEQ_7: 14;

        hence s in ( dom v) by A2, A17, A69;

      end;

      then ( dom ( reproj (2,xy0))) = REAL & (( reproj (2,xy0)) .: Ny0) c= ( dom v) by FUNCT_2:def 1, TARSKI:def 3;

      then

       A70: Ny0 c= ( dom (v * ( reproj (2,xy0)))) by FUNCT_3: 3;

      then

       A71: (v * ( reproj (2,xy0))) is_differentiable_in (( proj (2,2)) . xy0) by A14, A65, FDIFF_1:def 4;

      

       A72: for x be Element of REAL holds ((v * ( reproj (1,xy0))) . x) = (v . <*x, y0*>)

      proof

        let x be Element of REAL ;

        x in REAL ;

        then x in ( dom ( reproj (1,xy0))) by PDIFF_1:def 5;

        

        hence ((v * ( reproj (1,xy0))) . x) = (v . (( reproj (1,xy0)) . x)) by FUNCT_1: 13

        .= (v . ( Replace (xy0,1,x))) by PDIFF_1:def 5

        .= (v . <*x, y0*>) by A7, FINSEQ_7: 13;

      end;

      now

        let s be object;

        assume s in (( reproj (2,xy0)) .: Ny0);

        then

        consider y be Element of REAL such that

         A73: y in Ny0 and

         A74: s = (( reproj (2,xy0)) . y) by FUNCT_2: 65;

        

         A75: (x0 + (y * <i> )) in N by A46, A73;

        s = ( Replace (xy0,2,y)) by A74, PDIFF_1:def 5

        .= <*x0, y*> by A7, FINSEQ_7: 14;

        hence s in ( dom u) by A1, A17, A75;

      end;

      then ( dom ( reproj (2,xy0))) = REAL & (( reproj (2,xy0)) .: Ny0) c= ( dom u) by FUNCT_2:def 1, TARSKI:def 3;

      then

       A76: Ny0 c= ( dom (u * ( reproj (2,xy0)))) by FUNCT_3: 3;

      then

       A77: (u * ( reproj (2,xy0))) is_differentiable_in (( proj (2,2)) . xy0) by A14, A56, FDIFF_1:def 4;

      (LD3 . 1) = ( - (( Im ( diff (f,z0))) * 1)) by A16

      .= ( - ( Im ( diff (f,z0))));

      then

       A78: ( partdiff (u,xy0,2)) = ( - ( Im ( diff (f,z0)))) by A14, A56, A76, A77, FDIFF_1:def 5;

      

       A79: (LD1 . 1) = (( Re ( diff (f,z0))) * 1) by A11

      .= ( Re ( diff (f,z0)));

      

       A80: (( proj (1,2)) . xy0) = (xy0 . 1) by PDIFF_1:def 1

      .= x0 by A7, FINSEQ_1: 44;

      set Nx0 = ].(x0 - r0), (x0 + r0).[;

      reconsider Nx0 as Neighbourhood of x0 by A44, RCOMP_1:def 6;

      deffunc RF3( Real) = ( In ((( Im R) . $1), REAL ));

      consider R3 be Function of REAL , REAL such that

       A81: for y be Element of REAL holds (R3 . y) = RF3(y) from FUNCT_2:sch 4;

      

       A82: for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R3 /* h)) is convergent & ( lim ((h " ) (#) (R3 /* h))) = 0

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        ( rng h) c= COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

        then

        reconsider hz = h as Complex_Sequence by FUNCT_2: 6;

        reconsider hz as 0 -convergent non-zero Complex_Sequence by Lm3;

        now

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

          then

           A83: ( rng hz) c= ( dom R);

          let n be Nat;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          

           A84: ( Im ((h . nn) " )) = 0 & ( Re ((h . nn) " )) = ((h . nn) " ) by COMPLEX1:def 1, COMPLEX1:def 2;

          

           A85: ( dom R3) = REAL by PARTFUN1:def 2;

          then

           A86: ( rng h) c= ( dom R3);

          ( dom R3) c= ( dom ( Im R)) by A85, Th1, NUMBERS: 11;

          then

           A87: (h . nn) in ( dom ( Im R)) by A85, TARSKI:def 3;

          

          thus (((h " ) (#) (R3 /* h)) . n) = (((h " ) . n) * ((R3 /* h) . n)) by SEQ_1: 8

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

          .= (((h . nn) " ) * (R3 . (h . nn))) by A86, FUNCT_2: 108

          .= (((h . nn) " ) * RF3(.)) by A81

          .= (((h . n) " ) * (( Im R) . (h . n)))

          .= ((( Re ((h . n) " )) * ( Im (R /. (h . n)))) + (( Re (R /. (h . n))) * ( Im ((h . n) " )))) by A87, A84, COMSEQ_3:def 4

          .= ( Im (((h . n) " ) * (R /. (h . n)))) by COMPLEX1: 9

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

          .= ( Im (((hz " ) . nn) * ((R /* hz) . nn))) by A83, FUNCT_2: 109

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

        end;

        then

         A88: ((h " ) (#) (R3 /* h)) = ( Im ((hz " ) (#) (R /* hz))) by COMSEQ_3:def 6;

        ((hz " ) (#) (R /* hz)) is convergent & ( lim ((hz " ) (#) (R /* hz))) = 0 by CFDIFF_1:def 3;

        hence thesis by A88, COMPLEX1: 4, COMSEQ_3: 41;

      end;

      deffunc RF1( Real) = ( In ((( Re R) . $1), REAL ));

      consider R1 be Function of REAL , REAL such that

       A89: for x be Element of REAL holds (R1 . x) = RF1(x) from FUNCT_2:sch 4;

      reconsider R3 as RestFunc by A82, FDIFF_1:def 2;

      

       A90: for x be Real st x in Nx0 holds (x + (y0 * <i> )) in N

      proof

        let x be Real;

        assume x in Nx0;

        then |.(x - x0).| < r0 by RCOMP_1: 1;

        then (x + (y0 * <i> )) is Complex & |.((x + (y0 * <i> )) - z0).| < r0 by A6;

        then (x + (y0 * <i> )) in { y where y be Complex : |.(y - z0).| < r0 };

        hence (x + (y0 * <i> )) in N by A45;

      end;

      

       A91: for x be Real st x in Nx0 holds ((v . <*x, y0*>) - (v . <*x0, y0*>)) = ((( Im ( diff (f,z0))) * (x - x0)) + (( Im R) . ((x - x0) + ( 0 * <i> ))))

      proof

        let x be Real;

        ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))) in ( dom R) by A34, XCMPLX_0:def 2;

        then

         A92: (x - x0) in ( dom ( Im R)) by COMSEQ_3:def 4;

        assume x in Nx0;

        then

         A93: (x + (y0 * <i> )) in N by A90;

        then (x + (y0 * <i> )) in ( dom f) by A17;

        then

         A94: (x + (y0 * <i> )) in ( dom ( Im f)) by COMSEQ_3:def 4;

        

         A95: (x0 + (y0 * <i> )) in N by A6, CFDIFF_1: 7;

        then (x0 + (y0 * <i> )) in ( dom f) by A17;

        then

         A96: (x0 + (y0 * <i> )) in ( dom ( Im f)) by COMSEQ_3:def 4;

        ((v . <*x, y0*>) - (v . <*x0, y0*>)) = ((( Im f) . (x + (y0 * <i> ))) - (v . <*x0, y0*>)) by A2, A17, A93

        .= ((( Im f) . (x + (y0 * <i> ))) - (( Im f) . (x0 + (y0 * <i> )))) by A2, A17, A95

        .= (( Im (f . (x + (y0 * <i> )))) - (( Im f) . (x0 + (y0 * <i> )))) by A94, COMSEQ_3:def 4

        .= (( Im (f . (x + (y0 * <i> )))) - ( Im (f . (x0 + (y0 * <i> ))))) by A96, COMSEQ_3:def 4

        .= ( Im ((f . (x + (y0 * <i> ))) - (f . (x0 + (y0 * <i> ))))) by COMPLEX1: 19

        .= ( Im ((( diff (f,z0)) * ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))))) by A24, A93, A95

        .= (( Im (( diff (f,z0)) * ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) + ( Im (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))))) by COMPLEX1: 8

        .= (((( Im ( diff (f,z0))) * (x - x0)) + (( Re ( diff (f,z0))) * (y0 - y0))) + ( Im (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))))) by A58

        .= (((( Im ( diff (f,z0))) * (x - x0)) + (( Re ( diff (f,z0))) * (y0 - y0))) + ( Im (R . ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))))

        .= ((( Im ( diff (f,z0))) * (x - x0)) + (( Im R) . ((x - x0) + ( 0 * <i> )))) by A92, COMSEQ_3:def 4;

        hence thesis;

      end;

      

       A97: for x be Real st x in Nx0 holds (((v * ( reproj (1,xy0))) . x) - ((v * ( reproj (1,xy0))) . x0)) = ((LD2 . (x - x0)) + (R3 . (x - x0)))

      proof

        let x be Real;

        assume

         A98: x in Nx0;

        reconsider xx0 = (x - x0) as Element of REAL by XREAL_0:def 1;

        x in REAL by XREAL_0:def 1;

        

        hence (((v * ( reproj (1,xy0))) . x) - ((v * ( reproj (1,xy0))) . x0)) = ((v . <*x, y0*>) - ((v * ( reproj (1,xy0))) . x0)) by A72

        .= ((v . <*x, y0*>) - (v . <*x0, y0*>)) by A72

        .= ((( Im ( diff (f,z0))) * (x - x0)) + (( Im R) . ((x - x0) + ( 0 * <i> )))) by A91, A98

        .= ((LD2 . (x - x0)) + (( Im R) . ((x - x0) + ( 0 * <i> )))) by A9

        .= ((LD2 . (x - x0)) + RF3(xx0))

        .= ((LD2 . (x - x0)) + (R3 . xx0)) by A81

        .= ((LD2 . (x - x0)) + (R3 . (x - x0)));

      end;

      for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        ( rng h) c= COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

        then

        reconsider hz = h as Complex_Sequence by FUNCT_2: 6;

        reconsider hz as 0 -convergent non-zero Complex_Sequence by Lm3;

        now

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

          then

           A99: ( rng hz) c= ( dom R);

          let n be Nat;

          reconsider nn = n as Element of NAT by ORDINAL1:def 12;

          

           A100: ( Im ((h . nn) " )) = 0 & ( Re ((h . nn) " )) = ((h . nn) " ) by COMPLEX1:def 1, COMPLEX1:def 2;

          

           A101: ( dom R1) = REAL by PARTFUN1:def 2;

          then

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

          ( dom R1) c= ( dom ( Re R)) by A101, Th1, NUMBERS: 11;

          then

           A103: (h . nn) in ( dom ( Re R)) by A101, TARSKI:def 3;

          

          thus (((h " ) (#) (R1 /* h)) . n) = (((h " ) . n) * ((R1 /* h) . n)) by SEQ_1: 8

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

          .= (((h . nn) " ) * (R1 /. (h . nn))) by A102, FUNCT_2: 109

          .= (((h . nn) " ) * RF1(.)) by A89

          .= (((h . n) " ) * (( Re R) . (h . n)))

          .= ((( Re ((h . n) " )) * ( Re (R . (h . n)))) - (( Im ((h . n) " )) * ( Im (R . (h . n))))) by A103, A100, COMSEQ_3:def 3

          .= ( Re (((h . n) " ) * (R . (h . n)))) by COMPLEX1: 9

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

          .= ( Re (((hz " ) . nn) * ((R /* hz) . nn))) by A99, FUNCT_2: 109

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

        end;

        then

         A104: ((h " ) (#) (R1 /* h)) = ( Re ((hz " ) (#) (R /* hz))) by COMSEQ_3:def 5;

        ((hz " ) (#) (R /* hz)) is convergent & ( lim ((hz " ) (#) (R /* hz))) = 0 by CFDIFF_1:def 3;

        hence thesis by A104, COMPLEX1: 4, COMSEQ_3: 41;

      end;

      then

      reconsider R1 as RestFunc by FDIFF_1:def 2;

      

       A105: (LD2 . 1) = (( Im ( diff (f,z0))) * 1) by A9

      .= ( Im ( diff (f,z0)));

      

       A106: for x be Element of REAL holds ((u * ( reproj (1,xy0))) . x) = (u . <*x, y0*>)

      proof

        let x be Element of REAL ;

        x in REAL ;

        then x in ( dom ( reproj (1,xy0))) by PDIFF_1:def 5;

        

        hence ((u * ( reproj (1,xy0))) . x) = (u . (( reproj (1,xy0)) . x)) by FUNCT_1: 13

        .= (u . ( Replace (xy0,1,x))) by PDIFF_1:def 5

        .= (u . <*x, y0*>) by A7, FINSEQ_7: 13;

      end;

      

       A107: for x be Real st x in Nx0 holds ((u . <*x, y0*>) - (u . <*x0, y0*>)) = ((( Re ( diff (f,z0))) * (x - x0)) + (( Re R) . ((x - x0) + ( 0 * <i> ))))

      proof

        let x be Real;

        ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))) in ( dom R) by A34, XCMPLX_0:def 2;

        then

         A108: (x - x0) in ( dom ( Re R)) by COMSEQ_3:def 3;

        assume x in Nx0;

        then

         A109: (x + (y0 * <i> )) in N by A90;

        then (x + (y0 * <i> )) in ( dom f) by A17;

        then

         A110: (x + (y0 * <i> )) in ( dom ( Re f)) by COMSEQ_3:def 3;

        

         A111: (x0 + (y0 * <i> )) in N by A6, CFDIFF_1: 7;

        then (x0 + (y0 * <i> )) in ( dom f) by A17;

        then

         A112: (x0 + (y0 * <i> )) in ( dom ( Re f)) by COMSEQ_3:def 3;

        ((u . <*x, y0*>) - (u . <*x0, y0*>)) = ((( Re f) . (x + (y0 * <i> ))) - (u . <*x0, y0*>)) by A1, A17, A109

        .= ((( Re f) . (x + (y0 * <i> ))) - (( Re f) . (x0 + (y0 * <i> )))) by A1, A17, A111

        .= (( Re (f . (x + (y0 * <i> )))) - (( Re f) . (x0 + (y0 * <i> )))) by A110, COMSEQ_3:def 3

        .= (( Re (f . (x + (y0 * <i> )))) - ( Re (f . (x0 + (y0 * <i> ))))) by A112, COMSEQ_3:def 3

        .= ( Re ((f . (x + (y0 * <i> ))) - (f . (x0 + (y0 * <i> ))))) by COMPLEX1: 19

        .= ( Re ((( diff (f,z0)) * ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))))) by A24, A109, A111

        .= (( Re (( diff (f,z0)) * ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) + ( Re (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))))) by COMPLEX1: 8

        .= (((( Re ( diff (f,z0))) * (x - x0)) - (( Im ( diff (f,z0))) * (y0 - y0))) + ( Re (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))))) by A49

        .= (((( Re ( diff (f,z0))) * (x - x0)) - (( Im ( diff (f,z0))) * (y0 - y0))) + ( Re (R . ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))))

        .= ((( Re ( diff (f,z0))) * (x - x0)) + (( Re R) . ((x - x0) + ( 0 * <i> )))) by A108, COMSEQ_3:def 3;

        hence thesis;

      end;

      

       A113: for x be Real st x in Nx0 holds (((u * ( reproj (1,xy0))) . x) - ((u * ( reproj (1,xy0))) . x0)) = ((LD1 . (x - x0)) + (R1 . (x - x0)))

      proof

        let x be Real;

        assume

         A114: x in Nx0;

        reconsider xx0 = (x - x0) as Element of REAL by XREAL_0:def 1;

        x in REAL by XREAL_0:def 1;

        

        hence (((u * ( reproj (1,xy0))) . x) - ((u * ( reproj (1,xy0))) . x0)) = ((u . <*x, y0*>) - ((u * ( reproj (1,xy0))) . x0)) by A106

        .= ((u . <*x, y0*>) - (u . <*x0, y0*>)) by A106

        .= ((( Re ( diff (f,z0))) * (x - x0)) + (( Re R) . ((x - x0) + ( 0 * <i> )))) by A107, A114

        .= ((LD1 . (x - x0)) + (( Re R) . ((x - x0) + ( 0 * <i> )))) by A11

        .= ((LD1 . (x - x0)) + RF1(xx0))

        .= ((LD1 . (x - x0)) + (R1 . xx0)) by A89

        .= ((LD1 . (x - x0)) + (R1 . (x - x0)));

      end;

      now

        let s be object;

        assume s in (( reproj (1,xy0)) .: Nx0);

        then

        consider x be Element of REAL such that

         A115: x in Nx0 and

         A116: s = (( reproj (1,xy0)) . x) by FUNCT_2: 65;

        

         A117: (x + (y0 * <i> )) in N by A90, A115;

        s = ( Replace (xy0,1,x)) by A116, PDIFF_1:def 5

        .= <*x, y0*> by A7, FINSEQ_7: 13;

        hence s in ( dom v) by A2, A17, A117;

      end;

      then ( dom ( reproj (1,xy0))) = REAL & (( reproj (1,xy0)) .: Nx0) c= ( dom v) by FUNCT_2:def 1, TARSKI:def 3;

      then

       A118: Nx0 c= ( dom (v * ( reproj (1,xy0)))) by FUNCT_3: 3;

      then

       A119: (v * ( reproj (1,xy0))) is_differentiable_in (( proj (1,2)) . xy0) by A80, A97, FDIFF_1:def 4;

      now

        let s be object;

        assume s in (( reproj (1,xy0)) .: Nx0);

        then

        consider x be Element of REAL such that

         A120: x in Nx0 and

         A121: s = (( reproj (1,xy0)) . x) by FUNCT_2: 65;

        

         A122: (x + (y0 * <i> )) in N by A90, A120;

        s = ( Replace (xy0,1,x)) by A121, PDIFF_1:def 5

        .= <*x, y0*> by A7, FINSEQ_7: 13;

        hence s in ( dom u) by A1, A17, A122;

      end;

      then ( dom ( reproj (1,xy0))) = REAL & (( reproj (1,xy0)) .: Nx0) c= ( dom u) by FUNCT_2:def 1, TARSKI:def 3;

      then

       A123: Nx0 c= ( dom (u * ( reproj (1,xy0)))) by FUNCT_3: 3;

      then (u * ( reproj (1,xy0))) is_differentiable_in (( proj (1,2)) . xy0) by A80, A113, FDIFF_1:def 4;

      hence thesis by A80, A14, A113, A97, A65, A123, A77, A78, A105, A118, A119, A79, A70, A71, FDIFF_1:def 5;

    end;

    

     Lm6: for x,y be Real, vx,vy be Point of ( REAL-NS 1) st vx = <*x*> & vy = <*y*> holds (vx + vy) = <*(x + y)*> & (vx - vy) = <*(x - y)*>

    proof

      let x,y be Real, vx,vy be Point of ( REAL-NS 1);

      assume

       A1: vx = <*x*> & vy = <*y*>;

      reconsider vx1 = vx, vy1 = vy as Element of ( REAL 1) by REAL_NS1:def 4;

      

      thus (vx + vy) = (vx1 + vy1) by REAL_NS1: 2

      .= <*(x + y)*> by A1, RVSUM_1: 13;

      

      thus (vx - vy) = (vx1 - vy1) by REAL_NS1: 5

      .= <*(x - y)*> by A1, RVSUM_1: 29;

    end;

    

     Lm7: for x,y,z,w be Real, vx,vy be Element of ( REAL 2) st vx = <*x, y*> & vy = <*z, w*> holds (vx + vy) = <*(x + z), (y + w)*> & (vx - vy) = <*(x - z), (y - w)*>

    proof

      let x,y,z,w be Real, vx,vy be Element of ( REAL 2);

      reconsider x1 = x, y1 = y, z1 = z, w1 = w as Element of REAL by XREAL_0:def 1;

      assume

       A1: vx = <*x, y*> & vy = <*z, w*>;

      

      hence (vx + vy) = <*( addreal . (x1,z1)), ( addreal . (y1,w1))*> by FINSEQ_2: 75

      .= <*(x1 + z1), ( addreal . (y1,w1))*> by BINOP_2:def 9

      .= <*(x + z), (y + w)*> by BINOP_2:def 9;

      

      thus (vx - vy) = <*( diffreal . (x1,z1)), ( diffreal . (y1,w1))*> by A1, FINSEQ_2: 75

      .= <*(x1 - z1), ( diffreal . (y1,w1))*> by BINOP_2:def 10

      .= <*(x - z), (y - w)*> by BINOP_2:def 10;

    end;

    

     Lm8: for x,y,a be Real, vx be Element of ( REAL 2) st vx = <*x, y*> holds (a * vx) = <*(a * x), (a * y)*>

    proof

      let x,y,a be Real, vx be Element of ( REAL 2);

      reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def 1;

      assume vx = <*x, y*>;

      

      hence (a * vx) = <*((a multreal ) . x1), ((a multreal ) . y1)*> by FINSEQ_2: 36

      .= <*(a * x1), ((a multreal ) . y1)*> by RVSUM_1: 5

      .= <*(a * x), (a * y)*> by RVSUM_1: 5;

    end;

    

     Lm9: for x,y be Real holds <*x, y*> is Point of ( REAL-NS 2)

    proof

      let x,y be Real;

      reconsider x1 = x, y1 = y as Element of REAL by XREAL_0:def 1;

       <*x1, y1*> in ( REAL 2) by FINSEQ_2: 101;

      hence thesis by REAL_NS1:def 4;

    end;

    

     Lm10: for x,y,z,w be Real, vx,vy be Point of ( REAL-NS 2) st vx = <*x, y*> & vy = <*z, w*> holds (vx + vy) = <*(x + z), (y + w)*> & (vx - vy) = <*(x - z), (y - w)*>

    proof

      let x,y,z,w be Real, vx,vy be Point of ( REAL-NS 2);

      assume

       A1: vx = <*x, y*> & vy = <*z, w*>;

      reconsider vx1 = vx, vy1 = vy as Element of ( REAL 2) by REAL_NS1:def 4;

      

      thus (vx + vy) = (vx1 + vy1) by REAL_NS1: 2

      .= <*(x + z), (y + w)*> by A1, Lm7;

      

      thus (vx - vy) = (vx1 - vy1) by REAL_NS1: 5

      .= <*(x - z), (y - w)*> by A1, Lm7;

    end;

    

     Lm11: for x,y,a be Real, vx be Point of ( REAL-NS 2) st vx = <*x, y*> holds (a * vx) = <*(a * x), (a * y)*>

    proof

      let x,y,a be Real, vx be Point of ( REAL-NS 2);

      assume

       A1: vx = <*x, y*>;

      reconsider vx1 = vx as Element of ( REAL 2) by REAL_NS1:def 4;

      

      thus (a * vx) = (a * vx1) by REAL_NS1: 3

      .= <*(a * x), (a * y)*> by A1, Lm8;

    end;

    

     Lm12: for u be PartFunc of ( REAL 2), REAL , xy be Element of ( REAL 2) st xy in ( dom u) holds (( <>* u) . xy) = <*(u . xy)*>

    proof

      let u be PartFunc of ( REAL 2), REAL , xy be Element of ( REAL 2);

      assume xy in ( dom u);

      

      hence (( <>* u) . xy) = ((( proj (1,1)) qua Function " ) . (u . xy)) by FUNCT_1: 13

      .= <*(u . xy)*> by PDIFF_1: 1;

    end;

    

     Lm13: for u be PartFunc of ( REAL 2), REAL , x,y be Real st <*x, y*> in ( dom u) holds (( <>* u) /. <*x, y*>) = <*(u /. <*x, y*>)*>

    proof

      set W = (( proj (1,1)) qua Function " );

      let u be PartFunc of ( REAL 2), REAL ;

      let x,y be Real;

      assume

       A1: <*x, y*> in ( dom u);

      ( rng u) c= ( dom W) by PDIFF_1: 2;

      then ( dom ( <>* u)) = ( dom u) by RELAT_1: 27;

      

      hence (( <>* u) /. <*x, y*>) = (( <>* u) . <*x, y*>) by A1, PARTFUN1:def 6

      .= ((( proj (1,1)) qua Function " ) . (u . <*x, y*>)) by A1, FUNCT_1: 13

      .= <*(u . <*x, y*>)*> by PDIFF_1: 1

      .= <*(u /. <*x, y*>)*> by A1, PARTFUN1:def 6;

    end;

    

     Lm14: for x,y be Real, z be Complex, v be Element of ( REAL-NS 2) st z = (x + (y * <i> )) & v = <*x, y*> holds |.z.| = ||.v.||

    proof

      let x,y be Real, z be Complex, v be Element of ( REAL-NS 2);

      assume that

       A1: z = (x + (y * <i> )) and

       A2: v = <*x, y*>;

      

       A3: ( Im z) = y by A1, COMPLEX1: 12;

      x in REAL & y in REAL by XREAL_0:def 1;

      then

      reconsider xx = <*x, y*> as Element of ( REAL 2) by FINSEQ_2: 101;

      

       A4: |.xx.| = ||.v.|| & ( Re z) = x by A1, A2, COMPLEX1: 12, REAL_NS1: 1;

      reconsider xx1 = xx as Point of ( TOP-REAL 2) by EUCLID: 22;

      (xx1 `2 ) = y by FINSEQ_1: 44;

      then

       A5: (( sqr xx) . 2) = (y ^2 ) by VALUED_1: 11;

      (xx1 `1 ) = x by FINSEQ_1: 44;

      then ( len ( sqr xx)) = 2 & (( sqr xx) . 1) = (x ^2 ) by CARD_1:def 7, VALUED_1: 11;

      then ( sqr xx) = <*(x ^2 ), (y ^2 )*> by A5, FINSEQ_1: 44;

      hence thesis by A4, A3, RVSUM_1: 77;

    end;

    

     Lm15: for x,y be Real, z be Complex st z = (x + (y * <i> )) holds |.z.| <= ( |.x.| + |.y.|)

    proof

      let x,y be Real, z be Complex;

      assume z = (x + (y * <i> ));

      then ( Re z) = x & ( Im z) = y by COMPLEX1: 12;

      hence thesis by COMPLEX1: 78;

    end;

    

     Lm16: for x,y be Real holds |.x.| <= |.(x + (y * <i> )).| & |.y.| <= |.(x + (y * <i> )).|

    proof

      let x,y be Real;

      set z = (x + (y * <i> ));

      ( Re z) = x & ( Im z) = y by COMPLEX1: 12;

      hence thesis by COMPLEX1: 79;

    end;

    

     Lm17: for x,y be Real, v be Element of ( REAL-NS 2) st v = <*x, y*> holds ||.v.|| <= ( |.x.| + |.y.|)

    proof

      let x,y be Real, v be Element of ( REAL-NS 2);

      reconsider z = (x + (y * <i> )) as Complex;

      assume v = <*x, y*>;

      then |.z.| = ||.v.|| by Lm14;

      hence thesis by Lm15;

    end;

    theorem :: CFDIFF_2:3

    

     Th3: for seq be Real_Sequence holds seq is convergent & ( lim seq) = 0 iff ( abs seq) is convergent & ( lim ( abs seq)) = 0

    proof

      let seq be Real_Sequence;

      thus seq is convergent & ( lim seq) = 0 implies ( abs seq) is convergent & ( lim ( abs seq)) = 0

      proof

        assume that

         A1: seq is convergent and

         A2: ( lim seq) = 0 ;

        ( lim ( abs seq)) = |. 0 .| by A1, A2, SEQ_4: 14

        .= 0 by ABSVALUE: 2;

        hence thesis by A1;

      end;

      thus thesis by SEQ_4: 15;

    end;

    theorem :: CFDIFF_2:4

    

     Th4: for X be RealNormSpace, seq be sequence of X holds seq is convergent & ( lim seq) = ( 0. X) iff ||.seq.|| is convergent & ( lim ||.seq.||) = 0

    proof

      let X be RealNormSpace, seq be sequence of X;

      thus seq is convergent & ( lim seq) = ( 0. X) implies ||.seq.|| is convergent & ( lim ||.seq.||) = 0

      proof

        assume

         A1: seq is convergent & ( lim seq) = ( 0. X);

        then ( lim ||.seq.||) = ||.( 0. X).|| by LOPBAN_1: 20;

        hence thesis by A1, LOPBAN_1: 20, NORMSP_1: 1;

      end;

      assume

       A2: ||.seq.|| is convergent & ( lim ||.seq.||) = 0 ;

       A3:

      now

        let p be Real;

        assume 0 < p;

        then

        consider m be Nat such that

         A4: for n be Nat st m <= n holds |.(( ||.seq.|| . n) - 0 ).| < p by A2, SEQ_2:def 7;

        take m;

        hereby

          let n be Nat;

          assume m <= n;

          then |.(( ||.seq.|| . n) - 0 ).| < p by A4;

          then

           A5: |. ||.(seq . n).||.| < p by NORMSP_0:def 4;

           0 <= ||.(seq . n).|| by NORMSP_1: 4;

          then ||.(seq . n).|| < p by A5, ABSVALUE:def 1;

          hence ||.((seq . n) - ( 0. X)).|| < p by RLVECT_1: 13;

        end;

      end;

      then seq is convergent by NORMSP_1:def 6;

      hence thesis by A3, NORMSP_1:def 7;

    end;

    

     Lm18: for x be Real, vx be Element of ( REAL-NS 2) st vx = <*x, 0 *> holds ||.vx.|| = |.x.|

    proof

      let x be Real, vx be Element of ( REAL-NS 2);

      x in REAL & 0 in REAL by XREAL_0:def 1;

      then

      reconsider xx = <*x, 0 *> as Element of ( REAL 2) by FINSEQ_2: 101;

      reconsider xx1 = xx as Point of ( TOP-REAL 2) by EUCLID: 22;

      assume vx = <*x, 0 *>;

      then

       A1: ||.vx.|| = |.xx.| by REAL_NS1: 1;

      (xx1 `2 ) = 0 by FINSEQ_1: 44;

      then

       A2: (( sqr xx) . 2) = ( 0 ^2 ) by VALUED_1: 11;

      (xx1 `1 ) = x by FINSEQ_1: 44;

      then ( len ( sqr xx)) = 2 & (( sqr xx) . 1) = (x ^2 ) by CARD_1:def 7, VALUED_1: 11;

      then ( sqr xx) = <*(x ^2 ), ( 0 ^2 )*> by A2, FINSEQ_1: 44;

      

      then ( sqrt ( Sum ( sqr xx))) = ( sqrt ((x ^2 ) + ( 0 ^2 ))) by RVSUM_1: 77

      .= ( sqrt ((x ^2 ) + ( 0 * 0 ))) by SQUARE_1:def 1;

      hence ||.vx.|| = |.x.| by A1, COMPLEX1: 72;

    end;

    

     Lm19: for x be Real, vx be Element of ( REAL-NS 2) st vx = <* 0 , x*> holds ||.vx.|| = |.x.|

    proof

      let x be Real, vx be Element of ( REAL-NS 2);

      x in REAL & 0 in REAL by XREAL_0:def 1;

      then

      reconsider xx = <* 0 , x*> as Element of ( REAL 2) by FINSEQ_2: 101;

      reconsider xx1 = xx as Point of ( TOP-REAL 2) by EUCLID: 22;

      assume vx = <* 0 , x*>;

      then

       A1: ||.vx.|| = |.xx.| by REAL_NS1: 1;

      (xx1 `2 ) = x by FINSEQ_1: 44;

      then

       A2: (( sqr xx) . 2) = (x ^2 ) by VALUED_1: 11;

      (xx1 `1 ) = 0 by FINSEQ_1: 44;

      then ( len ( sqr xx)) = 2 & (( sqr xx) . 1) = ( 0 ^2 ) by CARD_1:def 7, VALUED_1: 11;

      then ( sqr xx) = <*( 0 ^2 ), (x ^2 )*> by A2, FINSEQ_1: 44;

      

      then ( sqrt ( Sum ( sqr xx))) = ( sqrt (( 0 ^2 ) + (x ^2 ))) by RVSUM_1: 77

      .= ( sqrt (( 0 * 0 ) + (x ^2 ))) by SQUARE_1:def 1

      .= ( sqrt (x ^2 ));

      hence ||.vx.|| = |.x.| by A1, COMPLEX1: 72;

    end;

    

     Lm20: for x be Real, vx be Element of ( REAL-NS 1) st vx = <*x*> holds ||.vx.|| = |.x.|

    proof

      let x be Real, vx be Element of ( REAL-NS 1);

      reconsider xx = vx as Element of ( REAL 1) by REAL_NS1:def 4;

      reconsider x2 = (x ^2 ) as Element of REAL by XREAL_0:def 1;

      assume vx = <*x*>;

      then ( sqrt ( Sum ( sqr xx))) = ( sqrt ( Sum <*x2*>)) by RVSUM_1: 55;

      then

       A1: ( sqrt ( Sum ( sqr xx))) = ( sqrt (x ^2 )) by RVSUM_1: 73;

       ||.vx.|| = |.xx.| by REAL_NS1: 1;

      hence ||.vx.|| = |.x.| by A1, COMPLEX1: 72;

    end;

    

     Lm21: for v be Element of ( REAL-NS 1) holds |.(( proj (1,1)) . v).| = ||.v.||

    proof

      let v be Element of ( REAL-NS 1);

      reconsider x = (( proj (1,1)) . v) as Real;

      reconsider w = v as Element of ( REAL 1) by REAL_NS1:def 4;

      ( len w) = 1 & (w . 1) = x by CARD_1:def 7, PDIFF_1:def 1;

      then <*x*> = w by FINSEQ_1: 40;

      hence thesis by Lm20;

    end;

    theorem :: CFDIFF_2:5

    

     Th5: for u be PartFunc of ( REAL 2), REAL , x0,y0 be Real, xy0 be Element of ( REAL 2) st xy0 = <*x0, y0*> & ( <>* u) is_differentiable_in xy0 holds u is_partial_differentiable_in (xy0,1) & u is_partial_differentiable_in (xy0,2) & <*( partdiff (u,xy0,1))*> = (( diff (( <>* u),xy0)) . <*1, 0 *>) & <*( partdiff (u,xy0,2))*> = (( diff (( <>* u),xy0)) . <* 0 , 1*>)

    proof

      reconsider ey0 = <* 0 , 1*> as Point of ( REAL-NS 2) by Lm9;

      reconsider ex0 = <*1, 0 *> as Point of ( REAL-NS 2) by Lm9;

      let u be PartFunc of ( REAL 2), REAL , x00,y00 be Real, xy0 be Element of ( REAL 2) such that

       A1: xy0 = <*x00, y00*> and

       A2: ( <>* u) is_differentiable_in xy0;

      reconsider x0 = x00, y0 = y00 as Element of REAL by XREAL_0:def 1;

      

       A3: xy0 = <*x0, y0*> by A1;

      set W = (( proj (1,1)) qua Function " );

      consider g be PartFunc of ( REAL-NS 2), ( REAL-NS 1), gxy0 be Point of ( REAL-NS 2) such that

       A4: ( <>* u) = g and

       A5: xy0 = gxy0 and

       A6: g is_differentiable_in gxy0 by A2;

      consider N be Neighbourhood of gxy0 such that

       A7: N c= ( dom g) and

       A8: ex R be RestFunc of ( REAL-NS 2), ( REAL-NS 1) st for xy be Point of ( REAL-NS 2) st xy in N holds ((g /. xy) - (g /. gxy0)) = ((( diff (g,gxy0)) . (xy - gxy0)) + (R /. (xy - gxy0))) by A6, NDIFF_1:def 7;

      consider R be RestFunc of ( REAL-NS 2), ( REAL-NS 1) such that

       A9: for xy be Point of ( REAL-NS 2) st xy in N holds ((g /. xy) - (g /. gxy0)) = ((( diff (g,gxy0)) . (xy - gxy0)) + (R /. (xy - gxy0))) by A8;

      consider r0 be Real such that

       A10: 0 < r0 and

       A11: { xy where xy be Point of ( REAL-NS 2) : ||.(xy - gxy0).|| < r0 } c= N by NFCONT_1:def 1;

      consider f be PartFunc of ( REAL-NS 2), ( REAL-NS 1), fxy0 be Point of ( REAL-NS 2) such that

       A12: ( <>* u) = f & xy0 = fxy0 and

       A13: ( diff (( <>* u),xy0)) = ( diff (f,fxy0)) by A2, PDIFF_1:def 8;

      ( rng u) c= ( dom W) by PDIFF_1: 2;

      then

       A14: ( dom ( <>* u)) = ( dom u) by RELAT_1: 27;

      

       A15: for xy be Element of ( REAL 2), L1,R1 be Real, z be Element of ( REAL 2) st xy in N & z = (xy - xy0) & <*L1*> = (( diff (( <>* u),xy0)) . z) & <*R1*> = (R . z) holds ((u . xy) - (u . xy0)) = (L1 + R1)

      proof

        let xy be Element of ( REAL 2), L1,R1 be Real, z be Element of ( REAL 2);

        assume that

         A16: xy in N and

         A17: z = (xy - xy0) and

         A18: <*L1*> = (( diff (( <>* u),xy0)) . z) and

         A19: <*R1*> = (R . z);

        reconsider zxy = xy as Point of ( REAL-NS 2) by REAL_NS1:def 4;

        

         A20: (zxy - gxy0) = z by A5, A17, REAL_NS1: 5;

        R is total by NDIFF_1:def 5;

        then ( dom R) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

        then (R /. (zxy - gxy0)) = <*R1*> by A19, A20, PARTFUN1:def 6;

        then

         A21: ((( diff (g,gxy0)) . (zxy - gxy0)) + (R /. (zxy - gxy0))) = <*(L1 + R1)*> by A4, A5, A12, A13, A18, A20, Lm6;

        

         A22: xy0 in N by A5, NFCONT_1: 4;

        

        then

         A23: (g /. gxy0) = (g . xy0) by A5, A7, PARTFUN1:def 6

        .= (( <>* u) /. xy0) by A4, A7, A22, PARTFUN1:def 6;

        

         A24: (g /. zxy) = (g . xy) by A7, A16, PARTFUN1:def 6

        .= (( <>* u) /. xy) by A4, A7, A16, PARTFUN1:def 6;

        

         A25: ((g /. zxy) - (g /. gxy0)) = ((( diff (g,gxy0)) . (zxy - gxy0)) + (R /. (zxy - gxy0))) by A9, A16;

        

         A26: (( <>* u) /. xy0) = (( <>* u) . xy0) by A4, A7, A22, PARTFUN1:def 6

        .= <*(u . xy0)*> by A4, A7, A14, A22, Lm12;

        (( <>* u) /. xy) = (( <>* u) . xy) by A4, A7, A16, PARTFUN1:def 6

        .= <*(u . xy)*> by A4, A7, A14, A16, Lm12;

        

        then ((g /. zxy) - (g /. gxy0)) = ( <*(u . xy)*> - <*(u . xy0)*>) by A24, A23, A26, REAL_NS1: 5

        .= ( <*(u . xy)*> + <*( - (u . xy0))*>) by RVSUM_1: 20

        .= <*((u . xy) - (u . xy0))*> by RVSUM_1: 13;

        

        hence ((u . xy) - (u . xy0)) = ( <*(L1 + R1)*> . 1) by A25, A21, FINSEQ_1:def 8

        .= (L1 + R1) by FINSEQ_1:def 8;

      end;

      set Nx0 = ].(x0 - r0), (x0 + r0).[;

      reconsider Nx0 as Neighbourhood of x0 by A10, RCOMP_1:def 6;

      

       A27: for x be Real st x in Nx0 holds <*x, y0*> in N

      proof

        let x be Real;

        reconsider xy = <*x, y0*> as Point of ( REAL-NS 2) by Lm9;

        (x - x0) in REAL & 0 in REAL by XREAL_0:def 1;

        then

        reconsider xx = <*(x - x0), 0 *> as Element of ( REAL 2) by FINSEQ_2: 101;

        reconsider xx1 = xx as Point of ( TOP-REAL 2) by EUCLID: 22;

        assume x in Nx0;

        then

         A28: |.(x - x0).| < r0 by RCOMP_1: 1;

        (xx1 `2 ) = 0 by FINSEQ_1: 44;

        then

         A29: |.(xx1 `2 ).| = 0 by ABSVALUE: 2;

        (xy - gxy0) = <*(x - x0), (y0 - y0)*> by A3, A5, Lm10

        .= <*(x - x0), 0 *>;

        then

         A30: ||.(xy - gxy0).|| = |.xx.| by REAL_NS1: 1;

         |.(xx1 `1 ).| = |.(x - x0).| & |.xx.| <= ( |.(xx1 `1 ).| + |.(xx1 `2 ).|) by FINSEQ_1: 44, JGRAPH_1: 31;

        then ||.(xy - gxy0).|| < r0 by A28, A29, A30, XXREAL_0: 2;

        then xy in { z where z be Point of ( REAL-NS 2) : ||.(z - gxy0).|| < r0 };

        hence thesis by A11;

      end;

      now

        let s be object;

        assume s in (( reproj (1,xy0)) .: Nx0);

        then

        consider x be Element of REAL such that

         A31: x in Nx0 and

         A32: s = (( reproj (1,xy0)) . x) by FUNCT_2: 65;

        

         A33: <*x, y0*> in N by A27, A31;

        s = ( Replace (xy0,1,x)) by A32, PDIFF_1:def 5

        .= <*x, y0*> by A3, FINSEQ_7: 13;

        hence s in ( dom u) by A4, A7, A14, A33;

      end;

      then ( dom ( reproj (1,xy0))) = REAL & (( reproj (1,xy0)) .: Nx0) c= ( dom u) by FUNCT_2:def 1, TARSKI:def 3;

      then

       A34: Nx0 c= ( dom (u * ( reproj (1,xy0)))) by FUNCT_3: 3;

      defpred P1[ Element of REAL , Element of REAL ] means ex vx be Element of ( REAL 2) st vx = <*$1, 0 *> & <*$2*> = (R . vx);

       A35:

      now

        let x be Element of REAL ;

        reconsider vx = <*x, ( In ( 0 , REAL ))*> as Element of ( REAL 2) by FINSEQ_2: 101;

        R is total by NDIFF_1:def 5;

        then

         A36: ( dom R) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

        vx is Element of ( REAL-NS 2) by REAL_NS1:def 4;

        then (R . vx) in the carrier of ( REAL-NS 1) by A36, PARTFUN1: 4;

        then (R . vx) is Element of ( REAL 1) by REAL_NS1:def 4;

        then

        consider y be Element of REAL such that

         A37: <*y*> = (R . vx) by FINSEQ_2: 97;

        take y;

        thus P1[x, y] by A37;

      end;

      consider R1 be Function of REAL , REAL such that

       A38: for x be Element of REAL holds P1[x, (R1 . x)] from FUNCT_2:sch 3( A35);

       A39:

      now

        let x be Real, vx be Element of ( REAL 2);

        assume

         A40: vx = <*x, 0 *>;

        x in REAL by XREAL_0:def 1;

        then ex vx1 be Element of ( REAL 2) st vx1 = <*x, 0 *> & <*(R1 . x)*> = (R . vx1) by A38;

        hence <*(R1 . x)*> = (R . vx) by A40;

      end;

      for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        defpred H1[ Nat, Element of ( REAL-NS 2)] means $2 = <*(h . $1), 0 *>;

         A41:

        now

          let n be Element of NAT ;

           <*(h . n), ( In ( 0 , REAL ))*> in ( REAL 2) by FINSEQ_2: 101;

          then

          reconsider y = <*(h . n), ( In ( 0 , REAL ))*> as Element of ( REAL-NS 2) by REAL_NS1:def 4;

          take y;

          thus H1[n, y];

        end;

        consider h1 be sequence of ( REAL-NS 2) such that

         A42: for n be Element of NAT holds H1[n, (h1 . n)] from FUNCT_2:sch 3( A41);

        

         A43: for n be Nat holds H1[n, (h1 . n)]

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A42;

        end;

        reconsider h1 as sequence of ( REAL-NS 2);

        now

          let n be Element of NAT ;

          

           A44: (h1 . n) = <*(h . n), 0 *> by A43;

          

          thus ( ||.h1.|| . n) = ||.(h1 . n).|| by NORMSP_0:def 4

          .= |.(h . n).| by A44, Lm18

          .= (( abs h) . n) by VALUED_1: 18;

        end;

        then

         A45: ||.h1.|| = ( abs h) by FUNCT_2: 63;

        set g = (( ||.h1.|| " ) (#) (R /* h1));

        now

          let n be Element of NAT ;

          reconsider v = (h1 . n) as Element of ( REAL 2) by REAL_NS1:def 4;

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

          then

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

          

           A47: (h1 . n) = <*(h . n), 0 *> by A43;

          R is total by NDIFF_1:def 5;

          then

           A48: ( dom R) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

          then

           A49: ( rng h1) c= ( dom R);

          

           A50: (h1 . n) = <*(h . n), 0 *> by A43;

          

           A51: (R /. (h1 . n)) = (R . v) by A48, PARTFUN1:def 6

          .= <*(R1 . (h . n))*> by A39, A47;

          

          thus ( ||.g.|| . n) = ||.(g . n).|| by NORMSP_0:def 4

          .= ||.((( ||.h1.|| " ) . n) * ((R /* h1) . n)).|| by NDIFF_1:def 2

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

          .= ||.(( ||.(h1 . n).|| " ) * ((R /* h1) . n)).|| by NORMSP_0:def 4

          .= ||.(( |.(h . n).| " ) * ((R /* h1) . n)).|| by A50, Lm18

          .= ||.(( |.(h . n).| " ) * (R /. (h1 . n))).|| by A49, FUNCT_2: 109

          .= ||.( |.((h . n) " ).| * (R /. (h1 . n))).|| by COMPLEX1: 66

          .= ( |. |.((h . n) " ).|.| * ||.(R /. (h1 . n)).||) by NORMSP_1:def 1

          .= ( |.((h . n) " ).| * |.(R1 . (h . n)).|) by A51, Lm20

          .= |.(((h . n) " ) * (R1 . (h . n))).| by COMPLEX1: 65

          .= |.(((h . n) " ) * ((R1 /* h) . n)).| by A46, FUNCT_2: 108

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

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

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

        end;

        then

         A52: ( abs ((h " ) (#) (R1 /* h))) = ||.g.|| by FUNCT_2: 63;

        now

          let n be Nat;

          

           A53: (h . n) <> 0 by SEQ_1: 5;

          

           A54: (h1 . n) = <*(h . n), 0 *> by A43;

          now

            assume (h1 . n) = ( 0. ( REAL-NS 2));

            

            then (h1 . n) = ( 0* 2) by REAL_NS1:def 4

            .= <* 0 , 0 *> by EUCLID: 54, EUCLID: 70;

            hence contradiction by A54, A53, FINSEQ_1: 77;

          end;

          hence (h1 . n) <> ( 0. ( REAL-NS 2));

        end;

        then

         A55: h1 is non-zero by NDIFF_1: 7;

        h is convergent & ( lim h) = 0 ;

        then ( abs h) is convergent & ( lim ( abs h)) = 0 by Th3;

        then h1 is convergent & ( lim h1) = ( 0. ( REAL-NS 2)) by A45, Th4;

        then h1 is ( 0. ( REAL-NS 2)) -convergent non-zero by A55, NDIFF_1:def 4;

        then (( ||.h1.|| " ) (#) (R /* h1)) is convergent & ( lim (( ||.h1.|| " ) (#) (R /* h1))) = ( 0. ( REAL-NS 1)) by NDIFF_1:def 5;

        then ||.g.|| is convergent & ( lim ||.g.||) = 0 by Th4;

        hence ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = 0 by A52, Th3;

      end;

      then

      reconsider R1 as RestFunc by FDIFF_1:def 2;

      ex0 is Element of ( REAL 2) by REAL_NS1:def 4;

      then (( diff (( <>* u),xy0)) . ex0) is Element of ( REAL 1) by FUNCT_2: 5;

      then

      consider Dux be Element of REAL such that

       A56: <*Dux*> = (( diff (( <>* u),xy0)) . ex0) by FINSEQ_2: 97;

      deffunc LDF1( Real) = ( In ((Dux * $1), REAL ));

      consider LD1 be Function of REAL , REAL such that

       A57: for x be Element of REAL holds (LD1 . x) = LDF1(x) from FUNCT_2:sch 4;

      

       A58: for x be Real holds (LD1 . x) = (Dux * x)

      proof

        let x be Real;

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

        (LD1 . x) = LDF1(x) by A57;

        hence thesis;

      end;

      set Ny0 = ].(y0 - r0), (y0 + r0).[;

      reconsider Ny0 as Neighbourhood of y0 by A10, RCOMP_1:def 6;

      

       A59: for y be Real st y in Ny0 holds <*x0, y*> in N

      proof

        let y be Real;

        reconsider xy = <*x0, y*> as Point of ( REAL-NS 2) by Lm9;

         0 in REAL & (y - y0) in REAL by XREAL_0:def 1;

        then

        reconsider xx = <* 0 , (y - y0)*> as Element of ( REAL 2) by FINSEQ_2: 101;

        reconsider xx1 = xx as Point of ( TOP-REAL 2) by EUCLID: 22;

        assume y in Ny0;

        then

         A60: |.(y - y0).| < r0 by RCOMP_1: 1;

        (xx1 `1 ) = 0 by FINSEQ_1: 44;

        then

         A61: |.(xx1 `1 ).| = 0 by ABSVALUE: 2;

         |.xx.| <= ( |.(xx1 `1 ).| + |.(xx1 `2 ).|) by JGRAPH_1: 31;

        then

         A62: |.xx.| <= |.(y - y0).| by A61, FINSEQ_1: 44;

        (xy - gxy0) = <*(x0 - x0), (y - y0)*> by A3, A5, Lm10

        .= <* 0 , (y - y0)*>;

        then ||.(xy - gxy0).|| = |.xx.| by REAL_NS1: 1;

        then ||.(xy - gxy0).|| < r0 by A60, A62, XXREAL_0: 2;

        then xy in { z where z be Point of ( REAL-NS 2) : ||.(z - gxy0).|| < r0 };

        hence thesis by A11;

      end;

      now

        let s be object;

        assume s in (( reproj (2,xy0)) .: Ny0);

        then

        consider y be Element of REAL such that

         A63: y in Ny0 and

         A64: s = (( reproj (2,xy0)) . y) by FUNCT_2: 65;

        

         A65: <*x0, y*> in N by A59, A63;

        s = ( Replace (xy0,2,y)) by A64, PDIFF_1:def 5

        .= <*x0, y*> by A3, FINSEQ_7: 14;

        hence s in ( dom u) by A4, A7, A14, A65;

      end;

      then ( dom ( reproj (2,xy0))) = REAL & (( reproj (2,xy0)) .: Ny0) c= ( dom u) by FUNCT_2:def 1, TARSKI:def 3;

      then

       A66: Ny0 c= ( dom (u * ( reproj (2,xy0)))) by FUNCT_3: 3;

      defpred P2[ Element of REAL , Element of REAL ] means ex vy be Element of ( REAL 2) st vy = <* 0 , $1*> & <*$2*> = (R . vy);

       A67:

      now

        let x be Element of REAL ;

        reconsider vx = <*( In ( 0 , REAL )), x*> as Element of ( REAL 2) by FINSEQ_2: 101;

        R is total by NDIFF_1:def 5;

        then

         A68: ( dom R) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

        vx is Element of ( REAL-NS 2) by REAL_NS1:def 4;

        then (R . vx) in the carrier of ( REAL-NS 1) by A68, PARTFUN1: 4;

        then (R . vx) is Element of ( REAL 1) by REAL_NS1:def 4;

        then

        consider y be Element of REAL such that

         A69: <*y*> = (R . vx) by FINSEQ_2: 97;

        take y;

        thus P2[x, y] by A69;

      end;

      consider R3 be Function of REAL , REAL such that

       A70: for x be Element of REAL holds P2[x, (R3 . x)] from FUNCT_2:sch 3( A67);

       A71:

      now

        let y be Real, vy be Element of ( REAL 2);

        reconsider yy = y as Element of REAL by XREAL_0:def 1;

        assume

         A72: vy = <* 0 , y*>;

        ex vy1 be Element of ( REAL 2) st vy1 = <* 0 , y*> & <*(R3 . yy)*> = (R . vy1) by A70;

        hence <*(R3 . y)*> = (R . vy) by A72;

      end;

      for h be 0 -convergent non-zero Real_Sequence holds ((h " ) (#) (R3 /* h)) is convergent & ( lim ((h " ) (#) (R3 /* h))) = 0

      proof

        let h be 0 -convergent non-zero Real_Sequence;

        defpred H1[ Nat, Element of ( REAL-NS 2)] means $2 = <* 0 , (h . $1)*>;

         A73:

        now

          let n be Element of NAT ;

           <*( In ( 0 , REAL )), (h . n)*> in ( REAL 2) by FINSEQ_2: 101;

          then

          reconsider y = <* 0 , (h . n)*> as Element of ( REAL-NS 2) by REAL_NS1:def 4;

          take y;

          thus H1[n, y];

        end;

        consider h1 be sequence of ( REAL-NS 2) such that

         A74: for n be Element of NAT holds H1[n, (h1 . n)] from FUNCT_2:sch 3( A73);

        

         A75: for n be Nat holds H1[n, (h1 . n)]

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A74;

        end;

        reconsider h1 as sequence of ( REAL-NS 2);

        now

          let n be Element of NAT ;

          

           A76: (h1 . n) = <* 0 , (h . n)*> by A75;

          

          thus ( ||.h1.|| . n) = ||.(h1 . n).|| by NORMSP_0:def 4

          .= |.(h . n).| by A76, Lm19

          .= (( abs h) . n) by VALUED_1: 18;

        end;

        then

         A77: ||.h1.|| = ( abs h) by FUNCT_2: 63;

        set g = (( ||.h1.|| " ) (#) (R /* h1));

        now

          let n be Element of NAT ;

          reconsider v = (h1 . n) as Element of ( REAL 2) by REAL_NS1:def 4;

          ( dom R3) = REAL by PARTFUN1:def 2;

          then

           A78: ( rng h) c= ( dom R3);

          

           A79: (h1 . n) = <* 0 , (h . n)*> by A75;

          R is total by NDIFF_1:def 5;

          then

           A80: ( dom R) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

          then

           A81: ( rng h1) c= ( dom R);

          

           A82: (h1 . n) = <* 0 , (h . n)*> by A75;

          

           A83: (R /. (h1 . n)) = (R . v) by A80, PARTFUN1:def 6

          .= <*(R3 . (h . n))*> by A71, A79;

          

          thus ( ||.g.|| . n) = ||.(g . n).|| by NORMSP_0:def 4

          .= ||.((( ||.h1.|| " ) . n) * ((R /* h1) . n)).|| by NDIFF_1:def 2

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

          .= ||.(( ||.(h1 . n).|| " ) * ((R /* h1) . n)).|| by NORMSP_0:def 4

          .= ||.(( |.(h . n).| " ) * ((R /* h1) . n)).|| by A82, Lm19

          .= ||.(( |.(h . n).| " ) * (R /. (h1 . n))).|| by A81, FUNCT_2: 109

          .= ||.( |.((h . n) " ).| * (R /. (h1 . n))).|| by COMPLEX1: 66

          .= ( |. |.((h . n) " ).|.| * ||.(R /. (h1 . n)).||) by NORMSP_1:def 1

          .= ( |.((h . n) " ).| * |.(R3 . (h . n)).|) by A83, Lm20

          .= |.(((h . n) " ) * (R3 . (h . n))).| by COMPLEX1: 65

          .= |.(((h . n) " ) * ((R3 /* h) . n)).| by A78, FUNCT_2: 108

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

          .= |.(((h " ) (#) (R3 /* h)) . n).| by VALUED_1: 5

          .= (( abs ((h " ) (#) (R3 /* h))) . n) by VALUED_1: 18;

        end;

        then

         A84: ( abs ((h " ) (#) (R3 /* h))) = ||.g.|| by FUNCT_2: 63;

        now

          let n be Nat;

          

           A85: (h . n) <> 0 by SEQ_1: 5;

          

           A86: (h1 . n) = <* 0 , (h . n)*> by A75;

          now

            assume (h1 . n) = ( 0. ( REAL-NS 2));

            

            then (h1 . n) = ( 0* 2) by REAL_NS1:def 4

            .= <* 0 , 0 *> by EUCLID: 54, EUCLID: 70;

            hence contradiction by A86, A85, FINSEQ_1: 77;

          end;

          hence (h1 . n) <> ( 0. ( REAL-NS 2));

        end;

        then

         A87: h1 is non-zero by NDIFF_1: 7;

        h is convergent & ( lim h) = 0 ;

        then ( abs h) is convergent & ( lim ( abs h)) = 0 by Th3;

        then h1 is convergent & ( lim h1) = ( 0. ( REAL-NS 2)) by A77, Th4;

        then h1 is ( 0. ( REAL-NS 2)) -convergent non-zero by A87, NDIFF_1:def 4;

        then (( ||.h1.|| " ) (#) (R /* h1)) is convergent & ( lim (( ||.h1.|| " ) (#) (R /* h1))) = ( 0. ( REAL-NS 1)) by NDIFF_1:def 5;

        then ||.g.|| is convergent & ( lim ||.g.||) = 0 by Th4;

        hence ((h " ) (#) (R3 /* h)) is convergent & ( lim ((h " ) (#) (R3 /* h))) = 0 by A84, Th3;

      end;

      then

      reconsider R3 as RestFunc by FDIFF_1:def 2;

      ey0 is Element of ( REAL 2) by REAL_NS1:def 4;

      then (( diff (( <>* u),xy0)) . ey0) is Element of ( REAL 1) by FUNCT_2: 5;

      then

      consider Duy be Element of REAL such that

       A88: <*Duy*> = (( diff (( <>* u),xy0)) . ey0) by FINSEQ_2: 97;

      deffunc LDF3( Real) = ( In ((Duy * $1), REAL ));

      consider LD3 be Function of REAL , REAL such that

       A89: for x be Element of REAL holds (LD3 . x) = LDF3(x) from FUNCT_2:sch 4;

      

       A90: for x be Real holds (LD3 . x) = (Duy * x)

      proof

        let x be Real;

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

        (LD3 . x) = LDF3(x) by A89;

        hence thesis;

      end;

      reconsider LD3 as LinearFunc by A90, FDIFF_1:def 3;

      

       A91: (LD3 . 1) = (Duy * 1) by A90

      .= Duy;

      

       A92: for y be Element of REAL holds ((u * ( reproj (2,xy0))) . y) = (u . <*x0, y*>)

      proof

        let y be Element of REAL ;

        y in REAL ;

        then y in ( dom ( reproj (2,xy0))) by PDIFF_1:def 5;

        

        hence ((u * ( reproj (2,xy0))) . y) = (u . (( reproj (2,xy0)) . y)) by FUNCT_1: 13

        .= (u . ( Replace (xy0,2,y))) by PDIFF_1:def 5

        .= (u . <*x0, y*>) by A3, FINSEQ_7: 14;

      end;

      

       A93: for y be Real st y in Ny0 holds (((u * ( reproj (2,xy0))) . y) - ((u * ( reproj (2,xy0))) . y0)) = ((LD3 . (y - y0)) + (R3 . (y - y0)))

      proof

        ey0 is Element of ( REAL 2) by REAL_NS1:def 4;

        then

        reconsider D1 = (( diff (( <>* u),xy0)) . ey0) as Element of ( REAL 1) by FUNCT_2: 5;

        let y be Real;

        assume

         A94: y in Ny0;

        reconsider yy = y as Element of REAL by XREAL_0:def 1;

        reconsider xy = <*x0, yy*> as Element of ( REAL 2) by FINSEQ_2: 101;

        

         A95: (LD3 . (y - y0)) = (Duy * (y - y0)) by A90;

        

         A96: (xy - xy0) = <*(x0 - x0), (y - y0)*> by A3, Lm7

        .= <*((y - y0) * 0 ), ((y - y0) * 1)*>

        .= ((y - y0) * ey0) by Lm11;

        

         A97: ( diff (f,fxy0)) is LinearOperator of ( REAL-NS 2), ( REAL-NS 1) by LOPBAN_1:def 9;

        ((y - y0) * D1) = ((y - y0) * (( diff (f,fxy0)) . ey0)) by A13, REAL_NS1: 3

        .= (( diff (( <>* u),xy0)) . (xy - xy0)) by A13, A96, A97, LOPBAN_1:def 5;

        then

         A98: <*(LD3 . (y - y0))*> = (( diff (( <>* u),xy0)) . (xy - xy0)) by A88, A95, RVSUM_1: 47;

         <* 0 , (y - y0)*> = <*(x0 - x0), (y - y0)*>

        .= (xy - xy0) by A3, Lm7;

        then

         A99: <*(R3 . (y - y0))*> = (R . (xy - xy0)) by A71;

        

        thus (((u * ( reproj (2,xy0))) . y) - ((u * ( reproj (2,xy0))) . y0)) = ((u . <*x0, yy*>) - ((u * ( reproj (2,xy0))) . y0)) by A92

        .= ((u . xy) - (u . xy0)) by A3, A92

        .= ((LD3 . (y - y0)) + (R3 . (y - y0))) by A15, A59, A94, A98, A99;

      end;

      reconsider LD1 as LinearFunc by A58, FDIFF_1:def 3;

      

       A100: (LD1 . 1) = (Dux * 1) by A58

      .= Dux;

      

       A101: for x be Element of REAL holds ((u * ( reproj (1,xy0))) . x) = (u . <*x, y0*>)

      proof

        let x be Element of REAL ;

        x in REAL ;

        then x in ( dom ( reproj (1,xy0))) by PDIFF_1:def 5;

        

        hence ((u * ( reproj (1,xy0))) . x) = (u . (( reproj (1,xy0)) . x)) by FUNCT_1: 13

        .= (u . ( Replace (xy0,1,x))) by PDIFF_1:def 5

        .= (u . <*x, y0*>) by A3, FINSEQ_7: 13;

      end;

      

       A102: for x be Real st x in Nx0 holds (((u * ( reproj (1,xy0))) . x) - ((u * ( reproj (1,xy0))) . x0)) = ((LD1 . (x - x0)) + (R1 . (x - x0)))

      proof

        ex0 is Element of ( REAL 2) by REAL_NS1:def 4;

        then

        reconsider D1 = (( diff (( <>* u),xy0)) . ex0) as Element of ( REAL 1) by FUNCT_2: 5;

        let x be Real;

        assume

         A103: x in Nx0;

        reconsider xx = x as Element of REAL by XREAL_0:def 1;

        reconsider xy = <*xx, y0*> as Element of ( REAL 2) by FINSEQ_2: 101;

        

         A104: (LD1 . (x - x0)) = (Dux * (x - x0)) by A58;

        

         A105: (xy - xy0) = <*(x - x0), (y0 - y0)*> by A3, Lm7

        .= <*((x - x0) * 1), ((x - x0) * 0 )*>

        .= ((x - x0) * ex0) by Lm11;

        

         A106: ( diff (f,fxy0)) is LinearOperator of ( REAL-NS 2), ( REAL-NS 1) by LOPBAN_1:def 9;

        ((x - x0) * D1) = ((x - x0) * (( diff (f,fxy0)) . ex0)) by A13, REAL_NS1: 3

        .= (( diff (( <>* u),xy0)) . (xy - xy0)) by A13, A105, A106, LOPBAN_1:def 5;

        then

         A107: <*(LD1 . (x - x0))*> = (( diff (( <>* u),xy0)) . (xy - xy0)) by A56, A104, RVSUM_1: 47;

         <*(x - x0), 0 *> = <*(x - x0), (y0 - y0)*>

        .= (xy - xy0) by A3, Lm7;

        then

         A108: <*(R1 . (x - x0))*> = (R . (xy - xy0)) by A39;

        

        thus (((u * ( reproj (1,xy0))) . x) - ((u * ( reproj (1,xy0))) . x0)) = ((u . <*xx, y0*>) - ((u * ( reproj (1,xy0))) . x0)) by A101

        .= ((u . xy) - (u . xy0)) by A3, A101

        .= ((LD1 . (x - x0)) + (R1 . (x - x0))) by A15, A27, A103, A107, A108;

      end;

      

       A109: (( proj (2,2)) . xy0) = (xy0 . 2) by PDIFF_1:def 1

      .= y0 by A3, FINSEQ_1: 44;

      then

       A110: (u * ( reproj (2,xy0))) is_differentiable_in (( proj (2,2)) . xy0) by A93, A66, FDIFF_1:def 4;

      

       A111: (( proj (1,2)) . xy0) = (xy0 . 1) by PDIFF_1:def 1

      .= x0 by A3, FINSEQ_1: 44;

      then (u * ( reproj (1,xy0))) is_differentiable_in (( proj (1,2)) . xy0) by A102, A34, FDIFF_1:def 4;

      hence thesis by A111, A109, A56, A88, A102, A93, A100, A34, A91, A66, A110, FDIFF_1:def 5;

    end;

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    theorem :: CFDIFF_2:6

    for f be PartFunc of COMPLEX , COMPLEX , u,v be PartFunc of ( REAL 2), REAL , z0 be Complex, x0,y0 be Real, xy0 be Element of ( REAL 2) st (for x,y be Real st <*x, y*> in ( dom v) holds (x + (y * <i> )) in ( dom f)) & (for x,y be Real st (x + (y * <i> )) in ( dom f) holds <*x, y*> in ( dom u) & (u . <*x, y*>) = (( Re f) . (x + (y * <i> )))) & (for x,y be Real st (x + (y * <i> )) in ( dom f) holds <*x, y*> in ( dom v) & (v . <*x, y*>) = (( Im f) . (x + (y * <i> )))) & z0 = (x0 + (y0 * <i> )) & xy0 = <*x0, y0*> & ( <>* u) is_differentiable_in xy0 & ( <>* v) is_differentiable_in xy0 & ( partdiff (u,xy0,1)) = ( partdiff (v,xy0,2)) & ( partdiff (u,xy0,2)) = ( - ( partdiff (v,xy0,1))) holds f is_differentiable_in z0 & u is_partial_differentiable_in (xy0,1) & u is_partial_differentiable_in (xy0,2) & v is_partial_differentiable_in (xy0,1) & v is_partial_differentiable_in (xy0,2) & ( Re ( diff (f,z0))) = ( partdiff (u,xy0,1)) & ( Re ( diff (f,z0))) = ( partdiff (v,xy0,2)) & ( Im ( diff (f,z0))) = ( - ( partdiff (u,xy0,2))) & ( Im ( diff (f,z0))) = ( partdiff (v,xy0,1))

    proof

      let f be PartFunc of COMPLEX , COMPLEX , u,v be PartFunc of ( REAL 2), REAL , z0 be Complex, x0,y0 be Real, xy0 be Element of ( REAL 2) such that

       A1: for x,y be Real st <*x, y*> in ( dom v) holds (x + (y * <i> )) in ( dom f) and

       A2: for x,y be Real st (x + (y * <i> )) in ( dom f) holds <*x, y*> in ( dom u) & (u . <*x, y*>) = (( Re f) . (x + (y * <i> ))) and

       A3: for x,y be Real st (x + (y * <i> )) in ( dom f) holds <*x, y*> in ( dom v) & (v . <*x, y*>) = (( Im f) . (x + (y * <i> ))) and

       A4: z0 = (x0 + (y0 * <i> )) and

       A5: xy0 = <*x0, y0*> and

       A6: ( <>* u) is_differentiable_in xy0 and

       A7: ( <>* v) is_differentiable_in xy0 and

       A8: ( partdiff (u,xy0,1)) = ( partdiff (v,xy0,2)) and

       A9: ( partdiff (u,xy0,2)) = ( - ( partdiff (v,xy0,1)));

      

       A10: ex hu be PartFunc of ( REAL-NS 2), ( REAL-NS 1), huxy0 be Point of ( REAL-NS 2) st ( <>* u) = hu & xy0 = huxy0 & ( diff (( <>* u),xy0)) = ( diff (hu,huxy0)) by A6, PDIFF_1:def 8;

      

       A11: ex hv be PartFunc of ( REAL-NS 2), ( REAL-NS 1), hvxy0 be Point of ( REAL-NS 2) st ( <>* v) = hv & xy0 = hvxy0 & ( diff (( <>* v),xy0)) = ( diff (hv,hvxy0)) by A7, PDIFF_1:def 8;

      consider gu be PartFunc of ( REAL-NS 2), ( REAL-NS 1), guxy0 be Point of ( REAL-NS 2) such that

       A12: ( <>* u) = gu and

       A13: xy0 = guxy0 and

       A14: gu is_differentiable_in guxy0 by A6;

      consider Nu be Neighbourhood of guxy0 such that

       A15: Nu c= ( dom gu) and

       A16: ex Ru be RestFunc of ( REAL-NS 2), ( REAL-NS 1) st for xy be Point of ( REAL-NS 2) st xy in Nu holds ((gu /. xy) - (gu /. guxy0)) = ((( diff (gu,guxy0)) . (xy - guxy0)) + (Ru /. (xy - guxy0))) by A14, NDIFF_1:def 7;

      consider r1 be Real such that

       A17: 0 < r1 and

       A18: { xy where xy be Point of ( REAL-NS 2) : ||.(xy - guxy0).|| < r1 } c= Nu by NFCONT_1:def 1;

      consider gv be PartFunc of ( REAL-NS 2), ( REAL-NS 1), gvxy0 be Point of ( REAL-NS 2) such that

       A19: ( <>* v) = gv and

       A20: xy0 = gvxy0 and

       A21: gv is_differentiable_in gvxy0 by A7;

      consider Ru be RestFunc of ( REAL-NS 2), ( REAL-NS 1) such that

       A22: for xy be Point of ( REAL-NS 2) st xy in Nu holds ((gu /. xy) - (gu /. guxy0)) = ((( diff (gu,guxy0)) . (xy - guxy0)) + (Ru /. (xy - guxy0))) by A16;

      

       A23: <*( partdiff (u,xy0,1))*> = (( diff (( <>* u),xy0)) . <*1, 0 *>) & <*( partdiff (u,xy0,2))*> = (( diff (( <>* u),xy0)) . <* 0 , 1*>) by A5, A6, Th5;

      

       A24: for x,y be Element of REAL st <*x, y*> in Nu holds ((u . <*x, y*>) - (u . <*x0, y0*>)) = (((( partdiff (u,xy0,1)) * (x - x0)) + (( partdiff (u,xy0,2)) * (y - y0))) + (( proj (1,1)) . (Ru . <*(x - x0), (y - y0)*>)))

      proof

        Ru is total by NDIFF_1:def 5;

        then

         A25: ( dom Ru) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

        ( rng u) c= ( dom (( proj (1,1)) qua Function " )) by PDIFF_1: 2;

        then

         A26: ( dom ( <>* u)) = ( dom u) by RELAT_1: 27;

         ||.(guxy0 - guxy0).|| < r1 by A17, NORMSP_1: 6;

        then guxy0 in { wxy where wxy be Point of ( REAL-NS 2) : ||.(wxy - guxy0).|| < r1 };

        then

         A27: <*x0, y0*> in Nu by A5, A13, A18;

        

        then (gu /. guxy0) = (gu . guxy0) by A5, A13, A15, PARTFUN1:def 6

        .= (( <>* u) /. <*x0, y0*>) by A5, A12, A13, A15, A27, PARTFUN1:def 6

        .= <*(u /. <*x0, y0*>)*> by A12, A15, A26, A27, Lm13

        .= <*(u . <*x0, y0*>)*> by A12, A15, A26, A27, PARTFUN1:def 6;

        then

         A28: (( proj (1,1)) . (gu /. guxy0)) = (u . <*x0, y0*>) by PDIFF_1: 1;

         <*( In ( 0 , REAL )), jj*> in ( REAL 2) by FINSEQ_2: 101;

        then

        reconsider e2 = <* 0 , 1*> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

         <*jj, ( In ( 0 , REAL ))*> in ( REAL 2) by FINSEQ_2: 101;

        then

        reconsider e1 = <*1, 0 *> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

        let x,y be Element of REAL ;

        

         A29: ( diff (gu,guxy0)) is LinearOperator of ( REAL-NS 2), ( REAL-NS 1) by LOPBAN_1:def 9;

         <*x, y*> in ( REAL 2) by FINSEQ_2: 101;

        then

        reconsider xy = <*x, y*> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

        

         A30: ((y - y0) * e2) = <*((y - y0) * 0 ), ((y - y0) * 1)*> by Lm11

        .= <* 0 , (y - y0)*>;

        

         A31: (xy - guxy0) = <*(x - x0), (y - y0)*> by A5, A13, Lm10;

        assume

         A32: <*x, y*> in Nu;

        

        then (gu /. xy) = (gu . xy) by A15, PARTFUN1:def 6

        .= (( <>* u) /. <*x, y*>) by A12, A15, A32, PARTFUN1:def 6

        .= <*(u /. <*x, y*>)*> by A12, A15, A32, A26, Lm13

        .= <*(u . <*x, y*>)*> by A12, A15, A32, A26, PARTFUN1:def 6;

        then (( proj (1,1)) . (gu /. xy)) = (u . <*x, y*>) by PDIFF_1: 1;

        

        then

         A33: ((u . <*x, y*>) - (u . <*x0, y0*>)) = (( proj (1,1)) . ((gu /. xy) - (gu /. guxy0))) by A28, PDIFF_1: 4

        .= (( proj (1,1)) . ((( diff (gu,guxy0)) . (xy - guxy0)) + (Ru /. (xy - guxy0)))) by A22, A32

        .= ((( proj (1,1)) . (( diff (gu,guxy0)) . (xy - guxy0))) + (( proj (1,1)) . (Ru /. (xy - guxy0)))) by PDIFF_1: 4;

        ((x - x0) * e1) = <*((x - x0) * 1), ((x - x0) * 0 )*> by Lm11

        .= <*(x - x0), 0 *>;

        

        then (((x - x0) * e1) + ((y - y0) * e2)) = <*((x - x0) + 0 ), ( 0 + (y - y0))*> by A30, Lm10

        .= <*(x - x0), (y - y0)*>;

        then (xy - guxy0) = (((x - x0) * e1) + ((y - y0) * e2)) by A5, A13, Lm10;

        

        then (( diff (gu,guxy0)) . (xy - guxy0)) = ((( diff (gu,guxy0)) . ((x - x0) * e1)) + (( diff (gu,guxy0)) . ((y - y0) * e2))) by A29, VECTSP_1:def 20

        .= (((x - x0) * (( diff (gu,guxy0)) . e1)) + (( diff (gu,guxy0)) . ((y - y0) * e2))) by A29, LOPBAN_1:def 5

        .= (((x - x0) * (( diff (gu,guxy0)) . e1)) + ((y - y0) * (( diff (gu,guxy0)) . e2))) by A29, LOPBAN_1:def 5;

        

        hence ((u . <*x, y*>) - (u . <*x0, y0*>)) = (((( proj (1,1)) . ((x - x0) * (( diff (gu,guxy0)) . e1))) + (( proj (1,1)) . ((y - y0) * (( diff (gu,guxy0)) . e2)))) + (( proj (1,1)) . (Ru /. (xy - guxy0)))) by A33, PDIFF_1: 4

        .= ((((x - x0) * (( proj (1,1)) . (( diff (gu,guxy0)) . e1))) + (( proj (1,1)) . ((y - y0) * (( diff (gu,guxy0)) . e2)))) + (( proj (1,1)) . (Ru /. (xy - guxy0)))) by PDIFF_1: 4

        .= ((((x - x0) * (( proj (1,1)) . <*( partdiff (u,xy0,1))*>)) + ((y - y0) * (( proj (1,1)) . <*( partdiff (u,xy0,2))*>))) + (( proj (1,1)) . (Ru /. (xy - guxy0)))) by A23, A12, A13, A10, PDIFF_1: 4

        .= ((((x - x0) * ( partdiff (u,xy0,1))) + ((y - y0) * (( proj (1,1)) . <*( partdiff (u,xy0,2))*>))) + (( proj (1,1)) . (Ru /. (xy - guxy0)))) by PDIFF_1: 1

        .= ((((x - x0) * ( partdiff (u,xy0,1))) + ((y - y0) * ( partdiff (u,xy0,2)))) + (( proj (1,1)) . (Ru /. (xy - guxy0)))) by PDIFF_1: 1

        .= (((( partdiff (u,xy0,1)) * (x - x0)) + (( partdiff (u,xy0,2)) * (y - y0))) + (( proj (1,1)) . (Ru . <*(x - x0), (y - y0)*>))) by A31, A25, PARTFUN1:def 6;

      end;

      consider Nv be Neighbourhood of gvxy0 such that

       A34: Nv c= ( dom gv) and

       A35: ex Rv be RestFunc of ( REAL-NS 2), ( REAL-NS 1) st for xy be Point of ( REAL-NS 2) st xy in Nv holds ((gv /. xy) - (gv /. gvxy0)) = ((( diff (gv,gvxy0)) . (xy - gvxy0)) + (Rv /. (xy - gvxy0))) by A21, NDIFF_1:def 7;

      consider r2 be Real such that

       A36: 0 < r2 and

       A37: { xy where xy be Point of ( REAL-NS 2) : ||.(xy - gvxy0).|| < r2 } c= Nv by NFCONT_1:def 1;

      set r0 = ( min ((r1 / 2),(r2 / 2)));

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

      consider Rv be RestFunc of ( REAL-NS 2), ( REAL-NS 1) such that

       A38: for xy be Point of ( REAL-NS 2) st xy in Nv holds ((gv /. xy) - (gv /. gvxy0)) = ((( diff (gv,gvxy0)) . (xy - gvxy0)) + (Rv /. (xy - gvxy0))) by A35;

      

       A39: <*( partdiff (v,xy0,1))*> = (( diff (( <>* v),xy0)) . <*1, 0 *>) & <*( partdiff (v,xy0,2))*> = (( diff (( <>* v),xy0)) . <* 0 , 1*>) by A5, A7, Th5;

      

       A40: for x,y be Element of REAL st <*x, y*> in Nv holds ((v . <*x, y*>) - (v . <*x0, y0*>)) = (((( partdiff (v,xy0,1)) * (x - x0)) + (( partdiff (v,xy0,2)) * (y - y0))) + (( proj (1,1)) . (Rv . <*(x - x0), (y - y0)*>)))

      proof

        Rv is total by NDIFF_1:def 5;

        then

         A41: ( dom Rv) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

        ( rng v) c= ( dom (( proj (1,1)) qua Function " )) by PDIFF_1: 2;

        then

         A42: ( dom ( <>* v)) = ( dom v) by RELAT_1: 27;

         ||.(gvxy0 - gvxy0).|| < r2 by A36, NORMSP_1: 6;

        then gvxy0 in { wxy where wxy be Point of ( REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 };

        then

         A43: <*x0, y0*> in Nv by A5, A20, A37;

        

        then (gv /. gvxy0) = (gv . gvxy0) by A5, A20, A34, PARTFUN1:def 6

        .= (( <>* v) /. <*x0, y0*>) by A5, A19, A20, A34, A43, PARTFUN1:def 6

        .= <*(v /. <*x0, y0*>)*> by A19, A34, A42, A43, Lm13

        .= <*(v . <*x0, y0*>)*> by A19, A34, A42, A43, PARTFUN1:def 6;

        then

         A44: (( proj (1,1)) . (gv /. gvxy0)) = (v . <*x0, y0*>) by PDIFF_1: 1;

         <*( In ( 0 , REAL )), jj*> in ( REAL 2) by FINSEQ_2: 101;

        then

        reconsider e2 = <* 0 , 1*> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

         <*jj, ( In ( 0 , REAL ))*> in ( REAL 2) by FINSEQ_2: 101;

        then

        reconsider e1 = <*1, 0 *> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

        let x,y be Element of REAL ;

        

         A45: ( diff (gv,gvxy0)) is LinearOperator of ( REAL-NS 2), ( REAL-NS 1) by LOPBAN_1:def 9;

         <*x, y*> in ( REAL 2) by FINSEQ_2: 101;

        then

        reconsider xy = <*x, y*> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

        

         A46: ((y - y0) * e2) = <*((y - y0) * 0 ), ((y - y0) * 1)*> by Lm11

        .= <* 0 , (y - y0)*>;

        

         A47: (xy - gvxy0) = <*(x - x0), (y - y0)*> by A5, A20, Lm10;

        assume

         A48: <*x, y*> in Nv;

        

        then (gv /. xy) = (gv . xy) by A34, PARTFUN1:def 6

        .= (( <>* v) /. <*x, y*>) by A19, A34, A48, PARTFUN1:def 6

        .= <*(v /. <*x, y*>)*> by A19, A34, A48, A42, Lm13

        .= <*(v . <*x, y*>)*> by A19, A34, A48, A42, PARTFUN1:def 6;

        then (( proj (1,1)) . (gv /. xy)) = (v . <*x, y*>) by PDIFF_1: 1;

        

        then

         A49: ((v . <*x, y*>) - (v . <*x0, y0*>)) = (( proj (1,1)) . ((gv /. xy) - (gv /. gvxy0))) by A44, PDIFF_1: 4

        .= (( proj (1,1)) . ((( diff (gv,gvxy0)) . (xy - gvxy0)) + (Rv /. (xy - gvxy0)))) by A38, A48

        .= ((( proj (1,1)) . (( diff (gv,gvxy0)) . (xy - gvxy0))) + (( proj (1,1)) . (Rv /. (xy - gvxy0)))) by PDIFF_1: 4;

        ((x - x0) * e1) = <*((x - x0) * 1), ((x - x0) * 0 )*> by Lm11

        .= <*(x - x0), 0 *>;

        

        then (((x - x0) * e1) + ((y - y0) * e2)) = <*((x - x0) + 0 ), ( 0 + (y - y0))*> by A46, Lm10

        .= <*(x - x0), (y - y0)*>;

        

        then (( diff (gv,gvxy0)) . (xy - gvxy0)) = ((( diff (gv,gvxy0)) . ((x - x0) * e1)) + (( diff (gv,gvxy0)) . ((y - y0) * e2))) by A47, A45, VECTSP_1:def 20

        .= (((x - x0) * (( diff (gv,gvxy0)) . e1)) + (( diff (gv,gvxy0)) . ((y - y0) * e2))) by A45, LOPBAN_1:def 5

        .= (((x - x0) * (( diff (gv,gvxy0)) . e1)) + ((y - y0) * (( diff (gv,gvxy0)) . e2))) by A45, LOPBAN_1:def 5;

        

        hence ((v . <*x, y*>) - (v . <*x0, y0*>)) = (((( proj (1,1)) . ((x - x0) * (( diff (gv,gvxy0)) . e1))) + (( proj (1,1)) . ((y - y0) * (( diff (gv,gvxy0)) . e2)))) + (( proj (1,1)) . (Rv /. (xy - gvxy0)))) by A49, PDIFF_1: 4

        .= ((((x - x0) * (( proj (1,1)) . (( diff (gv,gvxy0)) . e1))) + (( proj (1,1)) . ((y - y0) * (( diff (gv,gvxy0)) . e2)))) + (( proj (1,1)) . (Rv /. (xy - gvxy0)))) by PDIFF_1: 4

        .= ((((x - x0) * (( proj (1,1)) . (( diff (gv,gvxy0)) . e1))) + ((y - y0) * (( proj (1,1)) . (( diff (gv,gvxy0)) . e2)))) + (( proj (1,1)) . (Rv /. (xy - gvxy0)))) by PDIFF_1: 4

        .= ((((x - x0) * ( partdiff (v,xy0,1))) + ((y - y0) * (( proj (1,1)) . <*( partdiff (v,xy0,2))*>))) + (( proj (1,1)) . (Rv /. (xy - gvxy0)))) by A39, A19, A20, A11, PDIFF_1: 1

        .= ((((x - x0) * ( partdiff (v,xy0,1))) + ((y - y0) * ( partdiff (v,xy0,2)))) + (( proj (1,1)) . (Rv /. (xy - gvxy0)))) by PDIFF_1: 1

        .= (((( partdiff (v,xy0,1)) * (x - x0)) + (( partdiff (v,xy0,2)) * (y - y0))) + (( proj (1,1)) . (Rv . <*(x - x0), (y - y0)*>))) by A47, A41, PARTFUN1:def 6;

      end;

       A50:

      now

        let x,y be Element of REAL ;

        assume (x + (y * <i> )) in N;

        then

         A51: ex w be Complex st w = (x + (y * <i> )) & |.(w - z0).| < r0;

         <*x, y*> in ( REAL 2) by FINSEQ_2: 101;

        then

        reconsider xy = <*x, y*> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

        ( rng v) c= ( dom (( proj (1,1)) qua Function " )) by PDIFF_1: 2;

        then

         A52: ( dom ( <>* v)) = ( dom v) by RELAT_1: 27;

         ||.(gvxy0 - gvxy0).|| < r2 by A36, NORMSP_1: 6;

        then gvxy0 in { wxy where wxy be Point of ( REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 };

        then <*x0, y0*> in Nv by A5, A20, A37;

        then

         A53: (x0 + (y0 * <i> )) in ( dom f) by A1, A19, A34, A52;

        then

         A54: (x0 + (y0 * <i> )) in ( dom ( Re f)) by COMSEQ_3:def 3;

        

         A55: (x0 + (y0 * <i> )) in ( dom ( Im f)) by A53, COMSEQ_3:def 4;

        

         A56: (f . (x0 + (y0 * <i> ))) = (( Re (f . (x0 + (y0 * <i> )))) + (( Im (f . (x0 + (y0 * <i> )))) * <i> )) by COMPLEX1: 13

        .= ((( Re f) . (x0 + (y0 * <i> ))) + (( Im (f . (x0 + (y0 * <i> )))) * <i> )) by A54, COMSEQ_3:def 3

        .= ((( Re f) . (x0 + (y0 * <i> ))) + ((( Im f) . (x0 + (y0 * <i> ))) * <i> )) by A55, COMSEQ_3:def 4;

         |.(y - y0).| <= |.((x - x0) + ((y - y0) * <i> )).| by Lm16;

        then

         A57: |.(y - y0).| < r0 by A4, A51, XXREAL_0: 2;

        

         A58: r0 <= (r1 / 2) by XXREAL_0: 17;

        then

         A59: |.(y - y0).| < (r1 / 2) by A57, XXREAL_0: 2;

         |.(x - x0).| <= |.((x - x0) + ((y - y0) * <i> )).| by Lm16;

        then

         A60: |.(x - x0).| < r0 by A4, A51, XXREAL_0: 2;

        then |.(x - x0).| < (r1 / 2) by A58, XXREAL_0: 2;

        then

         A61: ( |.(x - x0).| + |.(y - y0).|) < ((r1 / 2) + (r1 / 2)) by A59, XREAL_1: 8;

        (xy - guxy0) = <*(x - x0), (y - y0)*> by A5, A13, Lm10;

        then ||.(xy - guxy0).|| <= ( |.(x - x0).| + |.(y - y0).|) by Lm17;

        then ||.(xy - guxy0).|| < r1 by A61, XXREAL_0: 2;

        then xy in { wxy where wxy be Point of ( REAL-NS 2) : ||.(wxy - guxy0).|| < r1 };

        

        then

         A62: ((u . <*x, y*>) - (u . <*x0, y0*>)) = (((( partdiff (u,xy0,1)) * (x - x0)) + (( partdiff (u,xy0,2)) * (y - y0))) + (( proj (1,1)) . (Ru . <*(x - x0), (y - y0)*>))) by A18, A24

        .= (((( partdiff (u,xy0,1)) * (x - x0)) + ((( <i> * ( partdiff (v,xy0,1))) * (y - y0)) * <i> )) + (( proj (1,1)) . (Ru . <*(x - x0), (y - y0)*>))) by A9;

        

         A63: r0 <= (r2 / 2) by XXREAL_0: 17;

        then

         A64: |.(y - y0).| < (r2 / 2) by A57, XXREAL_0: 2;

         |.(x - x0).| < (r2 / 2) by A63, A60, XXREAL_0: 2;

        then

         A65: ( |.(x - x0).| + |.(y - y0).|) < ((r2 / 2) + (r2 / 2)) by A64, XREAL_1: 8;

        (xy - gvxy0) = <*(x - x0), (y - y0)*> by A5, A20, Lm10;

        then ||.(xy - gvxy0).|| <= ( |.(x - x0).| + |.(y - y0).|) by Lm17;

        then ||.(xy - gvxy0).|| < r2 by A65, XXREAL_0: 2;

        then

         A66: xy in { wxy where wxy be Point of ( REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 };

        then

         A67: (((v . <*x, y*>) - (v . <*x0, y0*>)) * <i> ) = ((((( partdiff (v,xy0,1)) * (x - x0)) + (( partdiff (u,xy0,1)) * (y - y0))) + (( proj (1,1)) . (Rv . <*(x - x0), (y - y0)*>))) * <i> ) by A8, A37, A40;

         <*x, y*> in Nv by A37, A66;

        then

         A68: (x + (y * <i> )) in ( dom f) by A1, A19, A34, A52;

        then

         A69: (x + (y * <i> )) in ( dom ( Re f)) by COMSEQ_3:def 3;

        

         A70: (f /. (x + (y * <i> ))) = (f . (x + (y * <i> ))) & (f /. (x0 + (y0 * <i> ))) = (f . (x0 + (y0 * <i> ))) by A53, A68, PARTFUN1:def 6;

        

         A71: (x + (y * <i> )) in ( dom ( Im f)) by A68, COMSEQ_3:def 4;

        (f . (x + (y * <i> ))) = (( Re (f . (x + (y * <i> )))) + (( Im (f . (x + (y * <i> )))) * <i> )) by COMPLEX1: 13

        .= ((( Re f) . (x + (y * <i> ))) + (( Im (f . (x + (y * <i> )))) * <i> )) by A69, COMSEQ_3:def 3

        .= ((( Re f) . (x + (y * <i> ))) + ((( Im f) . (x + (y * <i> ))) * <i> )) by A71, COMSEQ_3:def 4;

        

        then ((f . (x + (y * <i> ))) - (f . (x0 + (y0 * <i> )))) = (((u . <*x, y*>) + ((( Im f) . (x + (y * <i> ))) * <i> )) - ((( Re f) . (x0 + (y0 * <i> ))) + ((( Im f) . (x0 + (y0 * <i> ))) * <i> ))) by A2, A68, A56

        .= (((u . <*x, y*>) + ((v . <*x, y*>) * <i> )) - ((( Re f) . (x0 + (y0 * <i> ))) + ((( Im f) . (x0 + (y0 * <i> ))) * <i> ))) by A3, A68

        .= (((u . <*x, y*>) + ((v . <*x, y*>) * <i> )) - ((u . <*x0, y0*>) + ((( Im f) . (x0 + (y0 * <i> ))) * <i> ))) by A2, A53

        .= (((u . <*x, y*>) + ((v . <*x, y*>) * <i> )) - ((u . <*x0, y0*>) + ((v . <*x0, y0*>) * <i> ))) by A3, A53

        .= (((u . <*x, y*>) - (u . <*x0, y0*>)) + (((v . <*x, y*>) - (v . <*x0, y0*>)) * <i> ));

        hence ((f /. (x + (y * <i> ))) - (f /. (x0 + (y0 * <i> )))) = (((( partdiff (u,xy0,1)) + ( <i> * ( partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * <i> ))) + ((( proj (1,1)) . (Ru . <*(x - x0), (y - y0)*>)) + ((( proj (1,1)) . (Rv . <*(x - x0), (y - y0)*>)) * <i> ))) by A70, A62, A67;

      end;

      

       A72: for x,y be Element of REAL st (x + (y * <i> )) in N holds |.(x - x0).| < (r1 / 2) & |.(y - y0).| < (r1 / 2) & |.(x - x0).| < (r2 / 2) & |.(y - y0).| < (r2 / 2)

      proof

        let x,y be Element of REAL ;

        assume (x + (y * <i> )) in N;

        then

         A73: ex w be Complex st w = (x + (y * <i> )) & |.(w - z0).| < r0;

         |.(x - x0).| <= |.((x - x0) + ((y - y0) * <i> )).| by Lm16;

        then

         A74: |.(x - x0).| < r0 by A4, A73, XXREAL_0: 2;

        

         A75: r0 <= (r1 / 2) by XXREAL_0: 17;

        hence |.(x - x0).| < (r1 / 2) by A74, XXREAL_0: 2;

         |.(y - y0).| <= |.((x - x0) + ((y - y0) * <i> )).| by Lm16;

        then

         A76: |.(y - y0).| < r0 by A4, A73, XXREAL_0: 2;

        hence |.(y - y0).| < (r1 / 2) by A75, XXREAL_0: 2;

        

         A77: r0 <= (r2 / 2) by XXREAL_0: 17;

        hence |.(x - x0).| < (r2 / 2) by A74, XXREAL_0: 2;

        thus |.(y - y0).| < (r2 / 2) by A77, A76, XXREAL_0: 2;

      end;

      reconsider N as Neighbourhood of z0 by A17, A36, CFDIFF_1: 6, XXREAL_0: 21;

      now

        let z be object;

        assume

         A78: z in N;

        then

        reconsider zz = z as Complex;

        set x = ( Re zz), y = ( Im zz);

        (x + (y * <i> )) in N by A78, COMPLEX1: 13;

        then |.(x - x0).| < (r2 / 2) & |.(y - y0).| < (r2 / 2) by A72;

        then

         A79: ( |.(x - x0).| + |.(y - y0).|) < ((r2 / 2) + (r2 / 2)) by XREAL_1: 8;

         <*x, y*> in ( REAL 2) by FINSEQ_2: 101;

        then

        reconsider xy = <*x, y*> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

        (xy - gvxy0) = <*(x - x0), (y - y0)*> by A5, A20, Lm10;

        then ||.(xy - gvxy0).|| <= ( |.(x - x0).| + |.(y - y0).|) by Lm17;

        then ||.(xy - gvxy0).|| < r2 by A79, XXREAL_0: 2;

        then xy in { wxy where wxy be Point of ( REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 };

        then

         A80: <*x, y*> in Nv by A37;

        ( rng v) c= ( dom (( proj (1,1)) qua Function " )) by PDIFF_1: 2;

        then z = (x + (y * <i> )) & ( dom ( <>* v)) = ( dom v) by COMPLEX1: 13, RELAT_1: 27;

        hence z in ( dom f) by A1, A19, A34, A80;

      end;

      then

       A81: N c= ( dom f) by TARSKI:def 3;

      defpred R0[ Complex, Complex] means $2 = ((( proj (1,1)) . (Ru . <*( Re $1), ( Im $1)*>)) + ((( proj (1,1)) . (Rv . <*( Re $1), ( Im $1)*>)) * <i> ));

      reconsider a = (( partdiff (u,xy0,1)) + ( <i> * ( partdiff (v,xy0,1)))) as Element of COMPLEX by XCMPLX_0:def 2;

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

      consider L be Function of COMPLEX , COMPLEX such that

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

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

      proof

        let z be Complex;

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

        (L /. z) = L0(z) by A82;

        hence thesis;

      end;

      then

      reconsider L as C_LinearFunc by CFDIFF_1:def 4;

       A83:

      now

        let z be Element of COMPLEX ;

        reconsider y = ((( proj (1,1)) . (Ru . <*( Re z), ( Im z)*>)) + ((( proj (1,1)) . (Rv . <*( Re z), ( Im z)*>)) * <i> )) as Element of COMPLEX by XCMPLX_0:def 2;

        take y;

        thus R0[z, y];

      end;

      consider R be Function of COMPLEX , COMPLEX such that

       A84: for z be Element of COMPLEX holds R0[z, (R . z)] from FUNCT_2:sch 3( A83);

      for h be 0 -convergent non-zero Complex_Sequence holds ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = 0

      proof

        let h be 0 -convergent non-zero Complex_Sequence;

         A85:

        now

          let r be Real;

          assume

           A86: 0 < r;

          Rv is total by NDIFF_1:def 5;

          then

          consider d2 be Real such that

           A87: d2 > 0 and

           A88: for z be Point of ( REAL-NS 2) st z <> ( 0. ( REAL-NS 2)) & ||.z.|| < d2 holds (( ||.z.|| " ) * ||.(Rv /. z).||) < (r / 2) by A86, NDIFF_1: 23;

          Ru is total by NDIFF_1:def 5;

          then

          consider d1 be Real such that

           A89: d1 > 0 and

           A90: for z be Point of ( REAL-NS 2) st z <> ( 0. ( REAL-NS 2)) & ||.z.|| < d1 holds (( ||.z.|| " ) * ||.(Ru /. z).||) < (r / 2) by A86, NDIFF_1: 23;

          set d = ( min (d1,d2));

          ( lim h) = 0 & 0 < d by A89, A87, CFDIFF_1:def 1, XXREAL_0: 21;

          then

          consider M be Nat such that

           A91: for n be Nat st M <= n holds |.((h . n) - 0 ).| < d by COMSEQ_2:def 6;

          

           A92: d <= d2 by XXREAL_0: 17;

          

           A93: d <= d1 by XXREAL_0: 17;

          now

            let n be Nat;

            reconsider nn = n as Element of NAT by ORDINAL1:def 12;

            set x = ( Re (h . nn)), y = ( Im (h . nn));

             <*x, y*> in ( REAL 2) by FINSEQ_2: 101;

            then

            reconsider z = <*x, y*> as Point of ( REAL-NS 2) by REAL_NS1:def 4;

            

             A94: z <> ( 0. ( REAL-NS 2))

            proof

              assume z = ( 0. ( REAL-NS 2));

              

              then z = ( 0* 2) by REAL_NS1:def 4

              .= <* 0 , 0 *> by EUCLID: 54, EUCLID: 70;

              then x = 0 & y = 0 by FINSEQ_1: 77;

              then (h . nn) = 0 by COMPLEX1: 4;

              hence contradiction by COMSEQ_1: 4;

            end;

            (h . nn) <> 0 by COMSEQ_1: 4;

            then

             A95: 0 < |.(h . n).| by COMPLEX1: 47;

            (R /. (h . n)) = ((( proj (1,1)) . (Ru . <*( Re (h . n)), ( Im (h . n))*>)) + ((( proj (1,1)) . (Rv . <*( Re (h . nn)), ( Im (h . nn))*>)) * <i> )) by A84;

            then

             A96: (( |.(h . n).| " ) * |.(R /. (h . n)).|) <= (( |.(h . n).| " ) * ( |.(( proj (1,1)) . (Ru . <*( Re (h . n)), ( Im (h . n))*>)).| + |.(( proj (1,1)) . (Rv . <*( Re (h . n)), ( Im (h . n))*>)).|)) by A95, Lm15, XREAL_1: 64;

            Ru is total by NDIFF_1:def 5;

            then ( dom Ru) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

            

            then

             A97: |.(( proj (1,1)) . (Ru . <*( Re (h . n)), ( Im (h . n))*>)).| = |.(( proj (1,1)) . (Ru /. z)).| by PARTFUN1:def 6

            .= ||.(Ru /. z).|| by Lm21;

            Rv is total by NDIFF_1:def 5;

            then ( dom Rv) = the carrier of ( REAL-NS 2) by PARTFUN1:def 2;

            

            then

             A98: |.(( proj (1,1)) . (Rv . <*( Re (h . n)), ( Im (h . n))*>)).| = |.(( proj (1,1)) . (Rv /. z)).| by PARTFUN1:def 6

            .= ||.(Rv /. z).|| by Lm21;

            (h . n) = (x + (y * <i> )) by COMPLEX1: 13;

            then

             A99: ||.z.|| = |.(h . n).| by Lm14;

            assume M <= n;

            then

             A100: |.((h . n) - 0 ).| < d by A91;

            then ||.z.|| < d2 by A92, A99, XXREAL_0: 2;

            then

             A101: (( ||.z.|| " ) * ||.(Rv /. z).||) < (r / 2) by A88, A94;

             ||.z.|| < d1 by A93, A100, A99, XXREAL_0: 2;

            then (( ||.z.|| " ) * ||.(Ru /. z).||) < (r / 2) by A90, A94;

            then ((( |.(h . n).| " ) * |.(( proj (1,1)) . (Ru . <*( Re (h . n)), ( Im (h . n))*>)).|) + (( |.(h . n).| " ) * |.(( proj (1,1)) . (Rv . <*( Re (h . n)), ( Im (h . n))*>)).|)) < ((r / 2) + (r / 2)) by A99, A101, A97, A98, XREAL_1: 8;

            then (( |.(h . n).| " ) * |.(R /. (h . n)).|) < r by A96, XXREAL_0: 2;

            then ( |.((h . n) " ).| * |.(R /. (h . n)).|) < r by COMPLEX1: 66;

            then

             A102: |.(((h . n) " ) * (R /. (h . n))).| < r by COMPLEX1: 65;

            ( dom R) = COMPLEX by FUNCT_2:def 1;

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

            then |.(((h . nn) " ) * ((R /* h) . nn)).| < r by A102, FUNCT_2: 109;

            then |.(((h " ) . n) * ((R /* h) . n)).| < r by VALUED_1: 10;

            hence |.((((h " ) (#) (R /* h)) . n) - 0 ).| < r by VALUED_1: 5;

          end;

          hence ex M be Nat st for n be Nat st M <= n holds |.((((h " ) (#) (R /* h)) . n) - 0c ).| < r;

        end;

        then ((h " ) (#) (R /* h)) is convergent by COMSEQ_2:def 5;

        hence thesis by A85, COMSEQ_2:def 6;

      end;

      then

      reconsider R as C_RestFunc by CFDIFF_1:def 3;

      now

        let z be Complex;

        set x = ( Re z), y = ( Im z);

        

         A103: z = (x + (y * <i> )) by COMPLEX1: 13;

        then

         A104: (z - z0) = ((x - x0) + ((y - y0) * <i> )) by A4;

        then ( Re (z - z0)) = (x - x0) by COMPLEX1: 12;

        then

         A105: <*( Re (z - z0)), ( Im (z - z0))*> = <*(x - x0), (y - y0)*> by A104, COMPLEX1: 12;

        

         A106: (z - z0) in COMPLEX by XCMPLX_0:def 2;

        assume z in N;

        

        hence ((f /. z) - (f /. z0)) = (((( partdiff (u,xy0,1)) + ( <i> * ( partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * <i> ))) + ((( proj (1,1)) . (Ru . <*(x - x0), (y - y0)*>)) + ((( proj (1,1)) . (Rv . <*(x - x0), (y - y0)*>)) * <i> ))) by A4, A50, A103

        .= ( L0(-) + ((( proj (1,1)) . (Ru . <*(x - x0), (y - y0)*>)) + ((( proj (1,1)) . (Rv . <*(x - x0), (y - y0)*>)) * <i> ))) by A4, A103

        .= ((L /. (z - z0)) + ((( proj (1,1)) . (Ru . <*(x - x0), (y - y0)*>)) + ((( proj (1,1)) . (Rv . <*(x - x0), (y - y0)*>)) * <i> ))) by A82, A106

        .= ((L /. (z - z0)) + (R /. (z - z0))) by A84, A105, A106;

      end;

      then f is_differentiable_in z0 by A81, CFDIFF_1:def 6;

      hence thesis by A2, A3, A4, A5, Th2;

    end;