fdiff_1.miz



    begin

    reserve y for object,

X for set;

    reserve x,x0,x1,x2,g,g1,g2,r,r1,s,p,p1 for Real;

    reserve n,m,k for Element of NAT ;

    reserve Y for Subset of REAL ;

    reserve Z for open Subset of REAL ;

    reserve s1,s3 for Real_Sequence;

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

    theorem :: FDIFF_1:1

    

     Th1: (for r holds r in Y iff r in REAL ) iff Y = REAL

    proof

      thus (for r holds r in Y iff r in REAL ) implies Y = REAL

      proof

        assume for r holds r in Y iff r in REAL ;

        then for y be object holds y in Y iff y in REAL ;

        hence thesis by TARSKI: 2;

      end;

      assume

       A1: Y = REAL ;

      let r;

      thus r in Y implies r in REAL ;

      thus thesis by A1;

    end;

    definition

      let x be Real;

      let IT be Real_Sequence;

      :: FDIFF_1:def1

      attr IT is x -convergent means

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

    end

    registration

      cluster 0 -convergent non-zero for Real_Sequence;

      existence

      proof

        deffunc F( Nat) = (1 / ($1 + 1));

        consider s1 such that

         A1: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

        take s1;

        now

          let n be Nat;

          ((n + 1) " ) <> 0 ;

          then (1 / (n + 1)) <> 0 by XCMPLX_1: 215;

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

        end;

        then

         A2: s1 is non-zero by SEQ_1: 5;

        ( lim s1) = 0 & s1 is convergent by A1, SEQ_4: 31;

        then s1 is 0 -convergent;

        hence thesis by A2;

      end;

    end

    registration

      let f be 0 -convergent Real_Sequence;

      cluster ( lim f) -> zero;

      coherence by Def1;

    end

    registration

      cluster 0 -convergent -> convergent for Real_Sequence;

      coherence ;

    end

    set cs = ( seq_const 0 );

    reserve h for non-zero 0 -convergent Real_Sequence;

    reserve c for constant Real_Sequence;

    definition

      let IT be PartFunc of REAL , REAL ;

      :: FDIFF_1:def2

      attr IT is RestFunc-like means

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

    end

    registration

      cluster RestFunc-like for PartFunc of REAL , REAL ;

      existence

      proof

        reconsider cf = ( REAL --> ( In ( 0 , REAL ))) as Function of REAL , REAL ;

        take f = cf;

        thus f is total;

        now

          let h;

          now

            let n be Nat;

            

             A2: ( rng h) c= ( dom f);

            

             A4: n in NAT by ORDINAL1:def 12;

            

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

            .= (((h " ) . n) * (f . (h . n))) by A4, A2, FUNCT_2: 108

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

            .= ( In ( 0 , REAL ));

          end;

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

          hence ((h " ) (#) (f /* h)) is convergent & ( lim ((h " ) (#) (f /* h))) = 0 by SEQ_4: 25;

        end;

        hence thesis;

      end;

    end

    definition

      mode RestFunc is RestFunc-like PartFunc of REAL , REAL ;

    end

    definition

      let IT be PartFunc of REAL , REAL ;

      :: FDIFF_1:def3

      attr IT is linear means

      : Def3: IT is total & ex r st for p holds (IT . p) = (r * p);

    end

    registration

      cluster linear for PartFunc of REAL , REAL ;

      existence

      proof

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

        defpred P[ set] means $1 in REAL ;

        consider f such that

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

        take f;

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

        then REAL c= ( dom f);

        then ( dom f) = REAL ;

        hence f is total by PARTFUN1:def 2;

        for p holds (f . p) = (1 * p)

        proof

          let p;

          ( In ((1 * p), REAL )) = (1 * p);

          hence thesis by A1;

        end;

        hence thesis;

      end;

    end

    definition

      mode LinearFunc is linear PartFunc of REAL , REAL ;

    end

    reserve R,R1,R2 for RestFunc;

    reserve L,L1,L2 for LinearFunc;

    theorem :: FDIFF_1:2

    

     Th2: (L1 + L2) is LinearFunc & (L1 - L2) is LinearFunc

    proof

      consider g1 such that

       A1: for p holds (L1 . p) = (g1 * p) by Def3;

      consider g2 such that

       A2: for p holds (L2 . p) = (g2 * p) by Def3;

      

       A3: L1 is total & L2 is total by Def3;

      now

        let p;

        reconsider pp = p as Element of REAL by XREAL_0:def 1;

        

        thus ((L1 + L2) . p) = ((L1 . pp) + (L2 . pp)) by A3, RFUNCT_1: 56

        .= ((g1 * p) + (L2 . p)) by A1

        .= ((g1 * p) + (g2 * p)) by A2

        .= ((g1 + g2) * p);

      end;

      hence (L1 + L2) is LinearFunc by A3, Def3;

      now

        let p;

        reconsider pp = p as Element of REAL by XREAL_0:def 1;

        

        thus ((L1 - L2) . p) = ((L1 . pp) - (L2 . pp)) by A3, RFUNCT_1: 56

        .= ((g1 * p) - (L2 . p)) by A1

        .= ((g1 * p) - (g2 * p)) by A2

        .= ((g1 - g2) * p);

      end;

      hence thesis by A3, Def3;

    end;

    theorem :: FDIFF_1:3

    

     Th3: (r (#) L) is LinearFunc

    proof

      consider g such that

       A1: for p holds (L . p) = (g * p) by Def3;

      

       A2: L is total by Def3;

      now

        let p;

        reconsider pp = p as Element of REAL by XREAL_0:def 1;

        

        thus ((r (#) L) . p) = (r * (L . pp)) by A2, RFUNCT_1: 57

        .= (r * (g * p)) by A1

        .= ((r * g) * p);

      end;

      hence thesis by A2, Def3;

    end;

    theorem :: FDIFF_1:4

    

     Th4: (R1 + R2) is RestFunc & (R1 - R2) is RestFunc & (R1 (#) R2) is RestFunc

    proof

      

       A1: R1 is total & R2 is total by Def2;

      now

        let h;

        

         A2: ((h " ) (#) ((R1 + R2) /* h)) = ((h " ) (#) ((R1 /* h) + (R2 /* h))) by A1, RFUNCT_2: 13

        .= (((h " ) (#) (R1 /* h)) + ((h " ) (#) (R2 /* h))) by SEQ_1: 16;

        

         A3: ((h " ) (#) (R1 /* h)) is convergent & ((h " ) (#) (R2 /* h)) is convergent by Def2;

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

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

        

        hence ( lim ((h " ) (#) ((R1 + R2) /* h))) = ( 0 + 0 ) by A3, A2, SEQ_2: 6

        .= 0 ;

      end;

      hence (R1 + R2) is RestFunc by A1, Def2;

      now

        let h;

        

         A4: ((h " ) (#) ((R1 - R2) /* h)) = ((h " ) (#) ((R1 /* h) - (R2 /* h))) by A1, RFUNCT_2: 13

        .= (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R2 /* h))) by SEQ_1: 21;

        

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

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

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

        

        hence ( lim ((h " ) (#) ((R1 - R2) /* h))) = ( 0 - 0 ) by A5, A4, SEQ_2: 12

        .= 0 ;

      end;

      hence (R1 - R2) is RestFunc by A1, Def2;

      now

        let h;

        

         A6: ((h " ) (#) (R2 /* h)) is convergent by Def2;

        

         A7: (h " ) is non-zero by SEQ_1: 33;

        

         A8: ((h " ) (#) (R1 /* h)) is convergent & h is convergent by Def2;

        then

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

        ( lim ((h " ) (#) (R1 /* h))) = 0 & ( lim h) = 0 by Def2;

        

        then

         A10: ( lim (h (#) ((h " ) (#) (R1 /* h)))) = ( 0 * 0 ) by A8, SEQ_2: 15

        .= 0 ;

        

         A11: ((h " ) (#) ((R1 (#) R2) /* h)) = (((R1 /* h) (#) (R2 /* h)) /" h) by A1, RFUNCT_2: 13

        .= ((((R1 /* h) (#) (R2 /* h)) (#) (h " )) /" (h (#) (h " ))) by A7, SEQ_1: 43

        .= ((((R1 /* h) (#) (R2 /* h)) (#) (h " )) (#) (((h " ) " ) (#) (h " ))) by SEQ_1: 36

        .= ((h (#) (h " )) (#) ((R1 /* h) (#) ((h " ) (#) (R2 /* h)))) by SEQ_1: 14

        .= (((h (#) (h " )) (#) (R1 /* h)) (#) ((h " ) (#) (R2 /* h))) by SEQ_1: 14

        .= ((h (#) ((h " ) (#) (R1 /* h))) (#) ((h " ) (#) (R2 /* h))) by SEQ_1: 14;

        hence ((h " ) (#) ((R1 (#) R2) /* h)) is convergent by A6, A9;

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

        

        hence ( lim ((h " ) (#) ((R1 (#) R2) /* h))) = ( 0 * 0 ) by A6, A9, A10, A11, SEQ_2: 15

        .= 0 ;

      end;

      hence thesis by A1, Def2;

    end;

    theorem :: FDIFF_1:5

    

     Th5: (r (#) R) is RestFunc

    proof

      

       A1: R is total by Def2;

      now

        let h;

        

         A2: ((h " ) (#) ((r (#) R) /* h)) = ((h " ) (#) (r (#) (R /* h))) by A1, RFUNCT_2: 14

        .= (r (#) ((h " ) (#) (R /* h))) by SEQ_1: 19;

        

         A3: ((h " ) (#) (R /* h)) is convergent by Def2;

        hence ((h " ) (#) ((r (#) R) /* h)) is convergent by A2;

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

        

        hence ( lim ((h " ) (#) ((r (#) R) /* h))) = (r * 0 ) by A3, A2, SEQ_2: 8

        .= 0 ;

      end;

      hence thesis by A1, Def2;

    end;

    theorem :: FDIFF_1:6

    

     Th6: (L1 (#) L2) is RestFunc-like

    proof

      consider x1 such that

       A1: for p holds (L1 . p) = (x1 * p) by Def3;

      

       A2: L1 is total & L2 is total by Def3;

      hence (L1 (#) L2) is total;

      consider x2 such that

       A3: for p holds (L2 . p) = (x2 * p) by Def3;

      now

        let h;

        now

          let n;

          

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

          

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

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

          .= (((h " ) . n) * ((L1 . (h . n)) * (L2 . (h . n)))) by A2, RFUNCT_1: 56

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

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

          .= ((((h . n) " ) * ((h . n) * x1)) * (L2 . (h . n))) by A1

          .= (((((h . n) " ) * (h . n)) * x1) * (L2 . (h . n)))

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

          .= (x1 * (x2 * (h . n))) by A3

          .= ((x1 * x2) * (h . n))

          .= (((x1 * x2) (#) h) . n) by SEQ_1: 9;

        end;

        then

         A5: ((h " ) (#) ((L1 (#) L2) /* h)) = ((x1 * x2) (#) h) by FUNCT_2: 63;

        thus ((h " ) (#) ((L1 (#) L2) /* h)) is convergent by A5;

        ( lim h) = 0 ;

        

        hence ( lim ((h " ) (#) ((L1 (#) L2) /* h))) = ((x1 * x2) * 0 ) by A5, SEQ_2: 8

        .= 0 ;

      end;

      hence thesis;

    end;

    theorem :: FDIFF_1:7

    

     Th7: (R (#) L) is RestFunc & (L (#) R) is RestFunc

    proof

      

       A1: L is total by Def3;

      consider x1 such that

       A2: for p holds (L . p) = (x1 * p) by Def3;

      

       A3: R is total by Def2;

       A4:

      now

        let h;

        

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

        now

          let n;

          

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

          .= (x1 * (h . n)) by A2

          .= ((x1 (#) h) . n) by SEQ_1: 9;

        end;

        then

         A6: (L /* h) = (x1 (#) h) by FUNCT_2: 63;

        

         A7: (L /* h) is convergent by A6;

        ( lim h) = 0 ;

        

        then

         A8: ( lim (L /* h)) = (x1 * 0 ) by A6, SEQ_2: 8

        .= 0 ;

        

         A9: ((h " ) (#) ((R (#) L) /* h)) = ((h " ) (#) ((R /* h) (#) (L /* h))) by A3, A1, RFUNCT_2: 13

        .= (((h " ) (#) (R /* h)) (#) (L /* h)) by SEQ_1: 14;

        hence ((h " ) (#) ((R (#) L) /* h)) is convergent by A7, A5;

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

        

        hence ( lim ((h " ) (#) ((R (#) L) /* h))) = ( 0 * 0 ) by A9, A7, A8, A5, SEQ_2: 15

        .= 0 ;

      end;

      hence (R (#) L) is RestFunc by A3, A1, Def2;

      thus thesis by A3, A1, A4, Def2;

    end;

    definition

      let f;

      let x0 be Real;

      :: FDIFF_1:def4

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

    end

    definition

      let f;

      let x0 be Real;

      assume

       A1: f is_differentiable_in x0;

      :: FDIFF_1:def5

      func diff (f,x0) -> Real means

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

      existence

      proof

        consider N be Neighbourhood of x0 such that

         A2: N c= ( dom f) and

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

        consider L, R such that

         A4: for x st x in N holds ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3;

        consider r such that

         A5: for p holds (L . p) = (r * p) by Def3;

        take r;

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

        .= r;

        hence thesis by A2, A4;

      end;

      uniqueness

      proof

        let r,s be Real;

        assume that

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

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

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

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

        consider L, R such that

         A9: r = (L . 1) and

         A10: for x st x in N holds ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A8;

        consider r1 such that

         A11: for p holds (L . p) = (r1 * p) by Def3;

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

         A12: ex L, R st s = (L . 1) & for x st x in N1 holds ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A7;

        consider L1, R1 such that

         A13: s = (L1 . 1) and

         A14: for x st x in N1 holds ((f . x) - (f . x0)) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A12;

        consider p1 such that

         A15: for p holds (L1 . p) = (p1 * p) by Def3;

        consider N0 be Neighbourhood of x0 such that

         A16: N0 c= N & N0 c= N1 by RCOMP_1: 17;

        consider g be Real such that

         A17: 0 < g and

         A18: N0 = ].(x0 - g), (x0 + g).[ by RCOMP_1:def 6;

        deffunc F( Nat) = (g / ($1 + 2));

        consider s1 such that

         A19: for n be Nat holds (s1 . n) = F(n) from SEQ_1:sch 1;

        now

          let n be Nat;

           0 <> (g / (n + 2)) by A17, XREAL_1: 139;

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

        end;

        then

         A20: s1 is non-zero by SEQ_1: 5;

        s1 is convergent & ( lim s1) = 0 by A19, SEQ_4: 31;

        then s1 is 0 -convergent;

        then

        reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A20;

        

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

        proof

          let n;

          take (x0 + (g / (n + 2)));

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

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

          then

           A22: (x0 + (g / (n + 2))) < (x0 + g) by XREAL_1: 6;

           0 < (g / (n + 2)) by A17, XREAL_1: 139;

          then (x0 + ( - g)) < (x0 + (g / (n + 2))) by A17, XREAL_1: 6;

          then (x0 + (g / (n + 2))) in ].(x0 - g), (x0 + g).[ by A22;

          hence thesis by A16, A18, A19;

        end;

        

         A23: s = (p1 * 1) by A13, A15;

        

         A24: r = (r1 * 1) by A9, A11;

         A25:

        now

          let x;

          assume that

           A26: x in N and

           A27: x in N1;

          ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A10, A26;

          then ((L . (x - x0)) + (R . (x - x0))) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A14, A27;

          then ((r1 * (x - x0)) + (R . (x - x0))) = ((L1 . (x - x0)) + (R1 . (x - x0))) by A11;

          hence ((r * (x - x0)) + (R . (x - x0))) = ((s * (x - x0)) + (R1 . (x - x0))) by A15, A24, A23;

        end;

        reconsider rs = (r - s) as Element of REAL by XREAL_0:def 1;

        now

          R1 is total by Def2;

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

          then

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

          let n be Nat;

          R is total by Def2;

          then ( dom R) = REAL by PARTFUN1:def 2;

          then

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

          

           A30: n in NAT by ORDINAL1:def 12;

          then ex x st x in N & x in N1 & (h . n) = (x - x0) by A21;

          then ((r * (h . n)) + (R . (h . n))) = ((s * (h . n)) + (R1 . (h . n))) by A25;

          then

           A31: (((r * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n))) = (((s * (h . n)) + (R1 . (h . n))) / (h . n)) by XCMPLX_1: 62;

          

           A32: ((R . (h . n)) / (h . n)) = ((R . (h . n)) * ((h . n) " )) by XCMPLX_0:def 9

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

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

          .= (((h " ) (#) (R /* h)) . n) by SEQ_1: 8;

          

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

          

           A34: ((R1 . (h . n)) / (h . n)) = ((R1 . (h . n)) * ((h . n) " )) by XCMPLX_0:def 9

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

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

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

          

           A35: ((s * (h . n)) / (h . n)) = (s * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (s * 1) by A33, XCMPLX_1: 60

          .= s;

          ((r * (h . n)) / (h . n)) = (r * ((h . n) / (h . n))) by XCMPLX_1: 74

          .= (r * 1) by A33, XCMPLX_1: 60

          .= r;

          then (r + ((R . (h . n)) / (h . n))) = (s + ((R1 . (h . n)) / (h . n))) by A31, A35, XCMPLX_1: 62;

          then r = (s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by A32, A34;

          hence rs = ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n) by RFUNCT_2: 1;

        end;

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

        then

         A36: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (r - s) by SEQ_4: 25;

        

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

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

        then (r - s) = ( 0 - 0 ) by A36, A37, SEQ_2: 12;

        hence thesis;

      end;

    end

    definition

      let f, X;

      :: FDIFF_1:def6

      pred f is_differentiable_on X means X c= ( dom f) & for x st x in X holds (f | X) is_differentiable_in x;

    end

    theorem :: FDIFF_1:8

    

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

    theorem :: FDIFF_1:9

    

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

    proof

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

      proof

        assume

         A1: f is_differentiable_on Z;

        hence Z c= ( dom f);

        let x0;

        assume

         A2: x0 in Z;

        then (f | Z) is_differentiable_in x0 by A1;

        then

        consider N be Neighbourhood of x0 such that

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

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

        take N;

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

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

        hence N c= ( dom f) by A3;

        consider L, R such that

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

        take L, R;

        let x;

        assume

         A6: x in N;

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

        then ((f . x) - ((f | Z) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3, A6, FUNCT_1: 47;

        hence thesis by A2, FUNCT_1: 49;

      end;

      assume that

       A7: Z c= ( dom f) and

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

      thus Z c= ( dom f) by A7;

      let x0;

      assume

       A9: x0 in Z;

      then

      consider N1 be Neighbourhood of x0 such that

       A10: N1 c= Z by RCOMP_1: 18;

      f is_differentiable_in x0 by A8, A9;

      then

      consider N be Neighbourhood of x0 such that

       A11: N c= ( dom f) and

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

      consider N2 be Neighbourhood of x0 such that

       A13: N2 c= N1 and

       A14: N2 c= N by RCOMP_1: 17;

      

       A15: N2 c= Z by A10, A13;

      take N2;

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

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

      hence

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

      consider L, R such that

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

      

       A18: x0 in N2 by RCOMP_1: 16;

      take L, R;

      let x;

      assume

       A19: x in N2;

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

      then (((f | Z) . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A16, A19, FUNCT_1: 47;

      hence thesis by A16, A18, FUNCT_1: 47;

    end;

    theorem :: FDIFF_1:10

    f is_differentiable_on Y implies Y is open

    proof

      assume

       A1: f is_differentiable_on Y;

      now

        let x0 be Element of REAL ;

        assume x0 in Y;

        then (f | Y) is_differentiable_in x0 by A1;

        then

        consider N be Neighbourhood of x0 such that

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

        take N;

        thus N c= Y by A2, XBOOLE_1: 1;

      end;

      hence thesis by RCOMP_1: 20;

    end;

    definition

      let f, X;

      assume

       A1: f is_differentiable_on X;

      :: FDIFF_1:def7

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

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

      existence

      proof

        deffunc F( Real) = ( In (( diff (f,$1)), REAL ));

        defpred P[ set] means $1 in X;

        consider F be PartFunc of REAL , REAL such that

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

        take F;

        now

          

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

          let y be object;

          assume y in X;

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

        end;

        then

         A4: X c= ( dom F);

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

        then ( dom F) c= X;

        hence ( dom F) = X by A4;

        for x st x in X holds (F . x) = ( diff (f,x))

        proof

          let x;

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

          x in X implies (F . x) = F(x) by A2;

          hence thesis;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be PartFunc of REAL , REAL ;

        assume that

         A5: ( dom F) = X and

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

         A7: ( dom G) = X and

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

        now

          let x be Element of REAL ;

          assume

           A9: x in ( dom F);

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

          hence (F . x) = (G . x) by A5, A8, A9;

        end;

        hence thesis by A5, A7, PARTFUN1: 5;

      end;

    end

    theorem :: FDIFF_1:11

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

    proof

      reconsider cf = ( REAL --> ( In ( 0 , REAL ))) as Function of REAL , REAL ;

      set R = cf;

      now

        let h;

         A2:

        now

          let n be Nat;

          

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

          

           A5: n in NAT by ORDINAL1:def 12;

          

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

          .= (((h " ) . n) * (R . (h . n))) by A5, A4, FUNCT_2: 108

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

          .= 0 ;

        end;

        then

         A6: ((h " ) (#) (R /* h)) is constant by VALUED_0:def 18;

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

        (((h " ) (#) (R /* h)) . 0 ) = 0 by A2;

        hence ( lim ((h " ) (#) (R /* h))) = 0 by A6, SEQ_4: 25;

      end;

      then

      reconsider R as RestFunc by Def2;

      set L = cf;

      for p holds (L . p) = ( 0 * p);

      then

      reconsider L as LinearFunc by Def3;

      assume

       A7: Z c= ( dom f);

      given r such that

       A8: ( rng f) = {r};

       A9:

      now

        let x0;

        assume x0 in ( dom f);

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

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

      end;

       A10:

      now

        let x0;

        assume

         A11: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A12: N c= Z by RCOMP_1: 18;

        

         A13: N c= ( dom f) by A7, A12;

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

        proof

          let x;

          reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

          assume x in N;

          

          hence ((f . x) - (f . x0)) = (r - (f . x0)) by A9, A13

          .= (r - r) by A7, A9, A11

          .= ((L . (xx - xx0)) + 0 )

          .= ((L . (x - x0)) + (R . (x - x0)));

        end;

        hence f is_differentiable_in x0 by A13;

      end;

      hence

       A14: f is_differentiable_on Z by A7, Th9;

      let x0;

      assume

       A15: x0 in Z;

      then

       A16: f is_differentiable_in x0 by A10;

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

      then

      consider N be Neighbourhood of x0 such that

       A17: N c= ( dom f);

      

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

      proof

        let x;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume x in N;

        

        hence ((f . x) - (f . x0)) = (r - (f . x0)) by A9, A17

        .= (r - r) by A7, A9, A15

        .= ((L . (xx - xx0)) + 0 )

        .= ((L . (x - x0)) + (R . (x - x0)));

      end;

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

      

      thus ((f `| Z) . x0) = ( diff (f,x0)) by A14, A15, Def7

      .= (L . j) by A16, A17, A18, Def5

      .= 0 ;

    end;

    registration

      let h be non-zero Real_Sequence;

      let n be Nat;

      cluster (h ^\ n) -> non-zero;

      coherence

      proof

        let hh be Real_Sequence such that

         A1: hh = (h ^\ n);

        ( rng hh) c= ( rng h) by A1, NAT_1: 55;

        hence not 0 in ( rng hh);

      end;

    end

    registration

      let h;

      let n be Nat;

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

      coherence

      proof

        ( lim h) = 0 ;

        then ( lim (h ^\ n)) = 0 by SEQ_4: 20;

        then (h ^\ n) is 0 -convergent;

        hence thesis;

      end;

    end

    theorem :: FDIFF_1:12

    

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

    proof

      let x0 be Real;

      let N be Neighbourhood of x0;

      assume that

       A1: f is_differentiable_in x0 and

       A2: N c= ( dom f);

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

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

      consider N2 be Neighbourhood of x0 such that

       A4: N2 c= N and

       A5: N2 c= N1 by RCOMP_1: 17;

      

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

      let h, c such that

       A7: ( rng c) = {x0} and

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

      consider g be Real such that

       A9: 0 < g and

       A10: N2 = ].(x0 - g), (x0 + g).[ by RCOMP_1:def 6;

      (x0 + 0 ) < (x0 + g) & (x0 - g) < (x0 - 0 ) by A9, XREAL_1: 8, XREAL_1: 15;

      then

       A11: x0 in N2 by A10;

      

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

      proof

        let y be object;

        assume y in ( rng c);

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

        then y in N by A4, A11;

        hence thesis by A2;

      end;

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

      proof

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

        then

         A13: ( lim c) = x0 by SEQ_4: 25;

        ( lim h) = 0 ;

        

        then ( lim (h + c)) = ( 0 + x0) by A13, SEQ_2: 6

        .= x0;

        then

        consider n be Nat such that

         A14: for m be Nat st n <= m holds |.(((h + c) . m) - x0).| < g by A9, SEQ_2:def 7;

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

        take n;

        

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

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

        let y be object;

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

        then

        consider m such that

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

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

        then

         A17: |.(((h + c) . (n + m)) - x0).| < g by A14;

        then (((h + c) . (m + n)) - x0) < g by SEQ_2: 1;

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

        then

         A18: (((h + c) ^\ n) . m) < (x0 + g) by XREAL_1: 19;

        ( - g) < (((h + c) . (m + n)) - x0) by A17, SEQ_2: 1;

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

        then (x0 + ( - g)) < (((h + c) ^\ n) . m) by XREAL_1: 20;

        hence thesis by A10, A16, A18;

      end;

      then

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

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

      consider L, R such that

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

      

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

      proof

        let y be object;

        assume

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

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

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

        then y in N by A4, A11;

        hence thesis by A2;

      end;

      

       A23: L is total by Def3;

      

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

      proof

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

        consider s1 such that

         A25: for k be Nat holds (s1 . k) = F(k) from SEQ_1:sch 1;

         A26:

        now

          

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

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

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

          take n1 = m;

          let k be Nat such that

           A29: n1 <= k;

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

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

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

        end;

        consider s such that

         A30: for p1 holds (L . p1) = (s * p1) by Def3;

        

         A31: (L . 1) = (s * 1) by A30

        .= s;

        now

          let m;

          

           A32: ((h ^\ n) . m) <> 0 by SEQ_1: 5;

          

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

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

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

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

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

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

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

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

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

          .= (s1 . m) by A25, A31;

        end;

        then

         A33: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = s1 by FUNCT_2: 63;

        hence (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) is convergent by A26, SEQ_2:def 6;

        hence thesis by A33, A26, SEQ_2:def 7;

      end;

      

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

      

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

      

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

      proof

        let k;

        (((h + c) ^\ n) . k) in ( rng ((h + c) ^\ n)) by VALUED_0: 28;

        then

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

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

        then

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

        ((((h + c) ^\ n) . k) - ((c ^\ n) . k)) = ((((h ^\ n) + (c ^\ n)) . k) - ((c ^\ n) . k)) by SEQM_3: 15

        .= ((((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k)) by SEQ_1: 7

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

        hence thesis by A20, A5, A37, A38;

      end;

      

       A39: R is total by Def2;

      now

        let k;

        

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

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

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

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

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

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

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

      end;

      then ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) = ((L /* (h ^\ n)) + (R /* (h ^\ n))) by FUNCT_2: 63;

      

      then

       A40: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = ((((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) " )) by A35, VALUED_0: 27

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

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

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

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

      then

       A41: (L . 1) = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) by A24, SEQ_4: 22;

      thus ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A24, A40, SEQ_4: 21;

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

      hence thesis by A1, A6, A41, Def5;

    end;

    theorem :: FDIFF_1:13

    

     Th13: f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies (f1 + f2) is_differentiable_in x0 & ( diff ((f1 + f2),x0)) = (( diff (f1,x0)) + ( diff (f2,x0)))

    proof

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

      assume that

       A1: f1 is_differentiable_in x0 and

       A2: f2 is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A3: N1 c= ( dom f1) and

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

      consider L1, R1 such that

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

      consider N2 be Neighbourhood of x0 such that

       A6: N2 c= ( dom f2) and

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

      consider L2, R2 such that

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

      reconsider R = (R1 + R2) as RestFunc by Th4;

      reconsider L = (L1 + L2) as LinearFunc by Th2;

      

       A9: L1 is total & L2 is total by Def3;

      consider N be Neighbourhood of x0 such that

       A10: N c= N1 and

       A11: N c= N2 by RCOMP_1: 17;

      

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

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

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

      then

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

      

       A14: R1 is total & R2 is total by Def2;

       A15:

      now

        let x;

        

         A16: x0 in N by RCOMP_1: 16;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume

         A17: x in N;

        

        hence (((f1 + f2) . x) - ((f1 + f2) . x0)) = (((f1 . x) + (f2 . x)) - ((f1 + f2) . x0)) by A13, VALUED_1:def 1

        .= (((f1 . x) + (f2 . x)) - ((f1 . x0) + (f2 . x0))) by A13, A16, VALUED_1:def 1

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

        .= (((L1 . (x - x0)) + (R1 . (x - x0))) + ((f2 . x) - (f2 . x0))) by A5, A10, A17

        .= (((L1 . (x - x0)) + (R1 . (x - x0))) + ((L2 . (x - x0)) + (R2 . (x - x0)))) by A8, A11, A17

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

        .= ((L . (x - x0)) + ((R1 . (xx - xx0)) + (R2 . (xx - xx0)))) by A9, RFUNCT_1: 56

        .= ((L . (x - x0)) + (R . (x - x0))) by A14, RFUNCT_1: 56;

      end;

      hence (f1 + f2) is_differentiable_in x0 by A13;

      

      hence ( diff ((f1 + f2),x0)) = (L . 1) by A13, A15, Def5

      .= ((L1 . j) + (L2 . j)) by A9, RFUNCT_1: 56

      .= (( diff (f1,x0)) + (L2 . 1)) by A1, A3, A5, Def5

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

    end;

    theorem :: FDIFF_1:14

    

     Th14: f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies (f1 - f2) is_differentiable_in x0 & ( diff ((f1 - f2),x0)) = (( diff (f1,x0)) - ( diff (f2,x0)))

    proof

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

      assume that

       A1: f1 is_differentiable_in x0 and

       A2: f2 is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A3: N1 c= ( dom f1) and

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

      consider L1, R1 such that

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

      consider N2 be Neighbourhood of x0 such that

       A6: N2 c= ( dom f2) and

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

      consider L2, R2 such that

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

      reconsider R = (R1 - R2) as RestFunc by Th4;

      reconsider L = (L1 - L2) as LinearFunc by Th2;

      

       A9: L1 is total & L2 is total by Def3;

      consider N be Neighbourhood of x0 such that

       A10: N c= N1 and

       A11: N c= N2 by RCOMP_1: 17;

      

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

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

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

      then

       A13: N c= ( dom (f1 - f2)) by VALUED_1: 12;

      

       A14: R1 is total & R2 is total by Def2;

       A15:

      now

        let x;

        

         A16: x0 in N by RCOMP_1: 16;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume

         A17: x in N;

        

        hence (((f1 - f2) . x) - ((f1 - f2) . x0)) = (((f1 . x) - (f2 . x)) - ((f1 - f2) . x0)) by A13, VALUED_1: 13

        .= (((f1 . x) - (f2 . x)) - ((f1 . x0) - (f2 . x0))) by A13, A16, VALUED_1: 13

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

        .= (((L1 . (x - x0)) + (R1 . (x - x0))) - ((f2 . x) - (f2 . x0))) by A5, A10, A17

        .= (((L1 . (x - x0)) + (R1 . (x - x0))) - ((L2 . (x - x0)) + (R2 . (x - x0)))) by A8, A11, A17

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

        .= ((L . (xx - xx0)) + ((R1 . (xx - xx0)) - (R2 . (xx - xx0)))) by A9, RFUNCT_1: 56

        .= ((L . (x - x0)) + (R . (x - x0))) by A14, RFUNCT_1: 56;

      end;

      hence (f1 - f2) is_differentiable_in x0 by A13;

      

      hence ( diff ((f1 - f2),x0)) = (L . 1) by A13, A15, Def5

      .= ((L1 . j) - (L2 . j)) by A9, RFUNCT_1: 56

      .= (( diff (f1,x0)) - (L2 . 1)) by A1, A3, A5, Def5

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

    end;

    theorem :: FDIFF_1:15

    

     Th15: f is_differentiable_in x0 implies (r (#) f) is_differentiable_in x0 & ( diff ((r (#) f),x0)) = (r * ( diff (f,x0)))

    proof

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

      assume

       A1: f is_differentiable_in x0;

      then

      consider N1 be Neighbourhood of x0 such that

       A2: N1 c= ( dom f) and

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

      consider L1, R1 such that

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

      reconsider R = (r (#) R1) as RestFunc by Th5;

      reconsider L = (r (#) L1) as LinearFunc by Th3;

      

       A5: L1 is total by Def3;

      

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

      

       A7: R1 is total by Def2;

       A8:

      now

        let x;

        

         A9: x0 in N1 by RCOMP_1: 16;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume

         A10: x in N1;

        

        hence (((r (#) f) . x) - ((r (#) f) . x0)) = ((r * (f . x)) - ((r (#) f) . x0)) by A6, VALUED_1:def 5

        .= ((r * (f . x)) - (r * (f . x0))) by A6, A9, VALUED_1:def 5

        .= (r * ((f . x) - (f . x0)))

        .= (r * ((L1 . (x - x0)) + (R1 . (x - x0)))) by A4, A10

        .= ((r * (L1 . (x - x0))) + (r * (R1 . (x - x0))))

        .= ((L . (xx - xx0)) + (r * (R1 . (xx - xx0)))) by A5, RFUNCT_1: 57

        .= ((L . (x - x0)) + (R . (x - x0))) by A7, RFUNCT_1: 57;

      end;

      hence (r (#) f) is_differentiable_in x0 by A6;

      

      hence ( diff ((r (#) f),x0)) = (L . 1) by A6, A8, Def5

      .= (r * (L1 . j)) by A5, RFUNCT_1: 57

      .= (r * ( diff (f,x0))) by A1, A2, A4, Def5;

    end;

    theorem :: FDIFF_1:16

    

     Th16: f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies (f1 (#) f2) is_differentiable_in x0 & ( diff ((f1 (#) f2),x0)) = (((f2 . x0) * ( diff (f1,x0))) + ((f1 . x0) * ( diff (f2,x0))))

    proof

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

      assume that

       A1: f1 is_differentiable_in x0 and

       A2: f2 is_differentiable_in x0;

      consider N1 be Neighbourhood of x0 such that

       A3: N1 c= ( dom f1) and

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

      consider L1, R1 such that

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

      consider N2 be Neighbourhood of x0 such that

       A6: N2 c= ( dom f2) and

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

      consider L2, R2 such that

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

      reconsider R18 = (R2 (#) L1) as RestFunc by Th7;

      reconsider R17 = (R1 (#) R2) as RestFunc by Th4;

      

       A9: R18 is total by Def2;

      reconsider R16 = (R1 (#) L2) as RestFunc by Th7;

      reconsider R14 = (L1 (#) L2) as RestFunc by Th6;

      reconsider R19 = (R16 + R17) as RestFunc by Th4;

      reconsider R20 = (R19 + R18) as RestFunc by Th4;

      

       A10: R14 is total by Def2;

      reconsider R12 = ((f1 . x0) (#) R2) as RestFunc by Th5;

      

       A11: R2 is total by Def2;

      reconsider L11 = ((f2 . x0) (#) L1) as LinearFunc by Th3;

      

       A12: L1 is total by Def3;

      reconsider R11 = ((f2 . x0) (#) R1) as RestFunc by Th5;

      

       A13: R1 is total by Def2;

      reconsider R13 = (R11 + R12) as RestFunc by Th4;

      reconsider R15 = (R13 + R14) as RestFunc by Th4;

      reconsider R = (R15 + R20) as RestFunc by Th4;

      consider N be Neighbourhood of x0 such that

       A14: N c= N1 and

       A15: N c= N2 by RCOMP_1: 17;

      

       A16: N c= ( dom f2) by A6, A15;

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

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

      then

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

      reconsider L12 = ((f1 . x0) (#) L2) as LinearFunc by Th3;

      

       A18: L2 is total by Def3;

      reconsider L = (L11 + L12) as LinearFunc by Th2;

      

       A19: R16 is total by Def2;

      

       A20: L11 is total & L12 is total by Def3;

       A21:

      now

        let x;

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

        assume

         A22: x in N;

        then

         A23: (((f1 . x) - (f1 . x0)) + (f1 . x0)) = (((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0)) by A5, A14;

        

        thus (((f1 (#) f2) . x) - ((f1 (#) f2) . x0)) = (((f1 . x) * (f2 . x)) - ((f1 (#) f2) . x0)) by VALUED_1: 5

        .= (((((f1 . x) * (f2 . x)) + ( - ((f1 . x) * (f2 . x0)))) + ((f1 . x) * (f2 . x0))) - ((f1 . x0) * (f2 . x0))) by VALUED_1: 5

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

        .= (((f1 . x) * ((f2 . x) - (f2 . x0))) + (((L1 . (x - x0)) + (R1 . (x - x0))) * (f2 . x0))) by A5, A14, A22

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

        .= (((f1 . xx) * ((f2 . xx) - (f2 . xx0))) + ((L11 . (xx - xx0)) + ((f2 . xx0) * (R1 . (xx - xx0))))) by A12, RFUNCT_1: 57

        .= (((((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0)) * ((f2 . x) - (f2 . x0))) + ((L11 . (x - x0)) + (R11 . (x - x0)))) by A13, A23, RFUNCT_1: 57

        .= (((((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0)))) by A8, A15, A22

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

        .= (((((L1 . (xx - xx0)) + (R1 . (xx - xx0))) * ((L2 . (xx - xx0)) + (R2 . (xx - xx0)))) + ((L12 . (xx - x0)) + ((f1 . x0) * (R2 . (xx - x0))))) + ((L11 . (xx - x0)) + (R11 . (xx - x0)))) by A18, RFUNCT_1: 57

        .= (((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + (R12 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0)))) by A11, RFUNCT_1: 57

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

        .= ((((L1 . (xx - x0)) + (R1 . (xx - x0))) * ((L2 . (xx - x0)) + (R2 . (xx - x0)))) + ((L12 . (xx - x0)) + ((L11 . (xx - x0)) + (R13 . (xx - xx0))))) by A13, A11, RFUNCT_1: 56

        .= ((((L1 . (xx - x0)) + (R1 . (xx - x0))) * ((L2 . (xx - x0)) + (R2 . (xx - x0)))) + (((L11 . (xx - x0)) + (L12 . (xx - x0))) + (R13 . (xx - xx0))))

        .= (((((L1 . (x - x0)) * (L2 . (x - x0))) + ((L1 . (x - x0)) * (R2 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0)))) by A20, RFUNCT_1: 56

        .= ((((R14 . (xx - x0)) + ((R2 . (x - x0)) * (L1 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . xxx0))) by A12, A18, RFUNCT_1: 56

        .= ((((R14 . (x - x0)) + (R18 . (x - x0))) + (((R1 . (x - x0)) * (L2 . (x - x0))) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (xx - xx0)))) by A12, A11, RFUNCT_1: 56

        .= ((((R14 . (xx - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . xxx0))) by A18, A13, RFUNCT_1: 56

        .= ((((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))) by A13, A11, RFUNCT_1: 56

        .= ((((R14 . (xx - xx0)) + (R18 . (x - x0))) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0)))) by A13, A11, A19, RFUNCT_1: 56

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

        .= (((L . xxx0) + (R13 . (x - xx0))) + ((R14 . (x - x0)) + (R20 . (x - x0)))) by A13, A11, A19, A9, RFUNCT_1: 56

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

        .= ((L . (xx - xx0)) + ((R15 . (x - x0)) + (R20 . (x - x0)))) by A13, A11, A10, RFUNCT_1: 56

        .= ((L . (x - x0)) + (R . (x - x0))) by A13, A11, A10, A19, A9, RFUNCT_1: 56;

      end;

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

      

      hence ( diff ((f1 (#) f2),x0)) = (L . 1) by A17, A21, Def5

      .= ((L11 . j) + (L12 . j)) by A20, RFUNCT_1: 56

      .= (((f2 . x0) * (L1 . j)) + (L12 . j)) by A12, RFUNCT_1: 57

      .= (((f2 . x0) * (L1 . 1)) + ((f1 . x0) * (L2 . 1))) by A18, RFUNCT_1: 57

      .= (((f2 . x0) * ( diff (f1,x0))) + ((f1 . x0) * (L2 . 1))) by A1, A3, A5, Def5

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

    end;

    theorem :: FDIFF_1:17

    

     Th17: Z c= ( dom f) & (f | Z) = ( id Z) implies f is_differentiable_on Z & for x st x in Z holds ((f `| Z) . x) = 1

    proof

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

      reconsider cf = ( REAL --> ( In ( 0 , REAL ))) as Function of REAL , REAL ;

      set R = cf;

      now

        let h;

         A2:

        now

          let n be Nat;

          

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

          

           A5: n in NAT by ORDINAL1:def 12;

          

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

          .= (((h " ) . n) * (R . (h . n))) by A5, A3, FUNCT_2: 108

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

          .= 0 ;

        end;

        then

         A6: ((h " ) (#) (R /* h)) is constant by VALUED_0:def 18;

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

        (((h " ) (#) (R /* h)) . 0 ) = 0 by A2;

        hence ( lim ((h " ) (#) (R /* h))) = 0 by A6, SEQ_4: 25;

      end;

      then

      reconsider R as RestFunc by Def2;

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

      for p holds (L . p) = (1 * p) by XREAL_0:def 1, FUNCT_1: 18;

      then

      reconsider L as LinearFunc by Def3;

      assume that

       A7: Z c= ( dom f) and

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

       A9:

      now

        let x;

        assume

         A10: x in Z;

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

        hence (f . x) = x by A10, FUNCT_1: 49;

      end;

       A11:

      now

        let x0;

        assume

         A12: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A13: N c= Z by RCOMP_1: 18;

        

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

        proof

          let x;

          reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

          assume x in N;

          

          hence ((f . x) - (f . x0)) = (x - (f . x0)) by A9, A13

          .= (x - x0) by A9, A12

          .= ((L . (xx - xx0)) + 0 )

          .= ((L . (x - x0)) + (R . (x - x0)));

        end;

        N c= ( dom f) by A7, A13;

        hence f is_differentiable_in x0 by A14;

      end;

      hence

       A15: f is_differentiable_on Z by A7, Th9;

      let x0;

      assume

       A16: x0 in Z;

      then

      consider N1 be Neighbourhood of x0 such that

       A17: N1 c= Z by RCOMP_1: 18;

      

       A18: f is_differentiable_in x0 by A11, A16;

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

      then

      consider N be Neighbourhood of x0 such that

       A19: N c= ( dom f);

      consider N2 be Neighbourhood of x0 such that

       A20: N2 c= N1 and

       A21: N2 c= N by RCOMP_1: 17;

      

       A22: N2 c= ( dom f) by A19, A21;

      

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

      proof

        let x;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume x in N2;

        then x in N1 by A20;

        

        hence ((f . x) - (f . x0)) = (x - (f . x0)) by A9, A17

        .= (x - x0) by A9, A16

        .= ((L . (xx - xx0)) + 0 )

        .= ((L . (x - x0)) + (R . (x - x0)));

      end;

      

      thus ((f `| Z) . x0) = ( diff (f,x0)) by A15, A16, Def7

      .= (L . j) by A18, A22, A23, Def5

      .= 1;

    end;

    theorem :: FDIFF_1:18

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

    proof

      assume that

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

       A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

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

        hence (f1 + f2) is_differentiable_in x0 by Th13;

      end;

      hence

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

      now

        let x;

        assume

         A4: x in Z;

        then

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

        

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

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

      end;

      hence thesis;

    end;

    theorem :: FDIFF_1:19

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

    proof

      assume that

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

       A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

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

        hence (f1 - f2) is_differentiable_in x0 by Th14;

      end;

      hence

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

      now

        let x;

        assume

         A4: x in Z;

        then

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

        

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

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

      end;

      hence thesis;

    end;

    theorem :: FDIFF_1:20

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

    proof

      assume that

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

       A2: f is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

        then f is_differentiable_in x0 by A2, Th9;

        hence (r (#) f) is_differentiable_in x0 by Th15;

      end;

      hence

       A3: (r (#) f) is_differentiable_on Z by A1, Th9;

      now

        let x;

        assume

         A4: x in Z;

        then

         A5: f is_differentiable_in x by A2, Th9;

        

        thus (((r (#) f) `| Z) . x) = ( diff ((r (#) f),x)) by A3, A4, Def7

        .= (r * ( diff (f,x))) by A5, Th15;

      end;

      hence thesis;

    end;

    theorem :: FDIFF_1:21

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

    proof

      assume that

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

       A2: f1 is_differentiable_on Z & f2 is_differentiable_on Z;

      now

        let x0;

        assume x0 in Z;

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

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

      end;

      hence

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

      now

        let x;

        assume

         A4: x in Z;

        then

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

        

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

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

      end;

      hence thesis;

    end;

    theorem :: FDIFF_1:22

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

    proof

      reconsider cf = ( REAL --> ( In ( 0 , REAL ))) as Function of REAL , REAL ;

      set R = cf;

      now

        let h;

         A2:

        now

          let n be Nat;

          

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

          

           A5: n in NAT by ORDINAL1:def 12;

          

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

          .= (((h " ) . n) * (R . (h . n))) by A5, A3, FUNCT_2: 108

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

          .= 0 ;

        end;

        then

         A6: ((h " ) (#) (R /* h)) is constant by VALUED_0:def 18;

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

        (((h " ) (#) (R /* h)) . 0 ) = 0 by A2;

        hence ( lim ((h " ) (#) (R /* h))) = 0 by A6, SEQ_4: 25;

      end;

      then

      reconsider R as RestFunc by Def2;

      set L = cf;

      for p holds (L . p) = ( 0 * p);

      then

      reconsider L as LinearFunc by Def3;

      assume that

       A7: Z c= ( dom f) and

       A8: (f | Z) is constant;

      consider r be Element of REAL such that

       A9: for x be Element of REAL st x in (Z /\ ( dom f)) holds (f . x) = r by A8, PARTFUN2: 57;

       A10:

      now

        let x0;

        assume

         A11: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A12: N c= Z by RCOMP_1: 18;

        

         A13: N c= ( dom f) by A7, A12;

        

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

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

        proof

          let x;

          reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

          assume x in N;

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

          

          hence ((f . x) - (f . x0)) = (r - (f . x0)) by A9

          .= (r - r) by A9, A14

          .= ((L . (xx - xx0)) + 0 )

          .= ((L . (x - x0)) + (R . (x - x0)));

        end;

        hence f is_differentiable_in x0 by A13;

      end;

      hence

       A15: f is_differentiable_on Z by A7, Th9;

      let x0;

      assume

       A16: x0 in Z;

      then

      consider N be Neighbourhood of x0 such that

       A17: N c= Z by RCOMP_1: 18;

      

       A18: N c= ( dom f) by A7, A17;

      

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

      

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

      proof

        let x;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume x in N;

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

        

        hence ((f . x) - (f . x0)) = (r - (f . x0)) by A9

        .= (r - r) by A9, A19

        .= ((L . (xx - xx0)) + 0 )

        .= ((L . (x - x0)) + (R . (x - x0)));

      end;

      

       A21: f is_differentiable_in x0 by A10, A16;

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

      

      thus ((f `| Z) . x0) = ( diff (f,x0)) by A15, A16, Def7

      .= (L . j) by A21, A18, A20, Def5

      .= 0 ;

    end;

    theorem :: FDIFF_1:23

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

    proof

      reconsider cf = ( REAL --> ( In ( 0 , REAL ))) as Function of REAL , REAL ;

      set R = cf;

      defpred P[ set] means $1 in REAL ;

      now

        let h;

         A2:

        now

          let n be Nat;

          

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

          

           A5: n in NAT by ORDINAL1:def 12;

          

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

          .= (((h " ) . n) * (R . (h . n))) by A5, A3, FUNCT_2: 108

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

          .= 0 ;

        end;

        then

         A6: ((h " ) (#) (R /* h)) is constant by VALUED_0:def 18;

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

        (((h " ) (#) (R /* h)) . 0 ) = 0 by A2;

        hence ( lim ((h " ) (#) (R /* h))) = 0 by A6, SEQ_4: 25;

      end;

      then

      reconsider R as RestFunc by Def2;

      assume that

       A7: Z c= ( dom f) and

       A8: for x st x in Z holds (f . x) = ((r * x) + p);

      deffunc G( Real) = ( In ((r * $1), REAL ));

      consider L be PartFunc of REAL , REAL such that

       A9: (for x be Element of REAL holds x in ( dom L) iff P[x]) & for x be Element of REAL st x in ( dom L) holds (L . x) = G(x) from SEQ_1:sch 3;

      for r holds r in ( dom L) iff r in REAL by A9;

      then ( dom L) = REAL by Th1;

      then

       A10: L is total by PARTFUN1:def 2;

      

       A11: for x holds (L . x) = (r * x)

      proof

        let x;

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

        (L . x) = G(x) by A9;

        hence thesis;

      end;

      then

      reconsider L as LinearFunc by A10, Def3;

       A12:

      now

        let x0;

        assume

         A13: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A14: N c= Z by RCOMP_1: 18;

        

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

        proof

          let x;

          reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

          assume x in N;

          

          hence ((f . x) - (f . x0)) = (((r * x) + p) - (f . x0)) by A8, A14

          .= (((r * x) + p) - ((r * x0) + p)) by A8, A13

          .= ((r * (x - x0)) + 0 )

          .= ((L . (xx - xx0)) + 0 ) by A11

          .= ((L . (x - x0)) + (R . (x - x0)));

        end;

        N c= ( dom f) by A7, A14;

        hence f is_differentiable_in x0 by A15;

      end;

      hence

       A16: f is_differentiable_on Z by A7, Th9;

      let x0;

      assume

       A17: x0 in Z;

      then

      consider N be Neighbourhood of x0 such that

       A18: N c= Z by RCOMP_1: 18;

      

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

      proof

        let x;

        reconsider xx = x, xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume x in N;

        

        hence ((f . x) - (f . x0)) = (((r * x) + p) - (f . x0)) by A8, A18

        .= (((r * x) + p) - ((r * x0) + p)) by A8, A17

        .= ((r * (x - x0)) + 0 )

        .= ((L . (xx - xx0)) + 0 ) by A11

        .= ((L . (x - x0)) + (R . (x - x0)));

      end;

      

       A20: N c= ( dom f) by A7, A18;

      

       A21: f is_differentiable_in x0 by A12, A17;

      

      thus ((f `| Z) . x0) = ( diff (f,x0)) by A16, A17, Def7

      .= (L . 1) by A21, A20, A19, Def5

      .= (r * 1) by A11

      .= r;

    end;

    theorem :: FDIFF_1:24

    

     Th24: for x0 be Real holds f is_differentiable_in x0 implies f is_continuous_in x0

    proof

      let x0 be Real;

      assume

       A1: f is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

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

      now

        consider g be Real such that

         A3: 0 < g and

         A4: N = ].(x0 - g), (x0 + g).[ by RCOMP_1:def 6;

        set s2 = ( seq_const x0);

        let s1 such that

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

         A6: s1 is convergent and

         A7: ( lim s1) = x0 and

         A8: for n be Nat holds (s1 . n) <> x0;

        consider l be Nat such that

         A9: for m be Nat st l <= m holds |.((s1 . m) - x0).| < g by A6, A7, A3, SEQ_2:def 7;

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

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

        consider s3 such that

         A10: for n be Nat holds (s3 . n) = G(n) from SEQ_1:sch 1;

        

         A11: s3 = (s1 - s2) by A10, RFUNCT_2: 1;

        then

         A12: s3 is convergent by A6;

        

         A13: ( rng c) = {x0}

        proof

          thus ( rng c) c= {x0}

          proof

            let y be object;

            assume y in ( rng c);

            then

            consider n such that

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

            

             A15: (s2 . (n + l)) = x0 by SEQ_1: 57;

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

            then y = x0 by A15;

            hence thesis by TARSKI:def 1;

          end;

          let y be object;

          assume y in {x0};

          then

           A16: y = x0 by TARSKI:def 1;

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

          .= y by A16, SEQ_1: 57;

          hence thesis by VALUED_0: 28;

        end;

         A17:

        now

          let p be Real such that

           A18: 0 < p;

          reconsider n = 0 as Nat;

          take n;

          let m be Nat such that n <= m;

          

           A19: m in NAT by ORDINAL1:def 12;

          x0 in N by RCOMP_1: 16;

          then ( rng c) c= ( dom f) by A2, A13, ZFMISC_1: 31;

          

          then |.(((f /* c) . m) - (f . x0)).| = |.((f . (c . m)) - (f . x0)).| by FUNCT_2: 108, A19

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

          .= |.((f . x0) - (f . x0)).| by SEQ_1: 57

          .= 0 by ABSVALUE: 2;

          hence |.(((f /* c) . m) - (f . x0)).| < p by A18;

        end;

        then

         A20: (f /* c) is convergent by SEQ_2:def 6;

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

        .= x0 by SEQ_1: 57;

        

        then ( lim s3) = (x0 - x0) by A6, A7, A11, SEQ_2: 12

        .= 0 ;

        then

         A21: ( lim (s3 ^\ l)) = 0 by A12, SEQ_4: 20;

         A22:

        now

          given n be Nat such that

           A23: (s3 . n) = 0 ;

          ((s1 . n) - (s2 . n)) = 0 by A10, A23;

          hence contradiction by A8, SEQ_1: 57;

        end;

         A24:

        now

          given n be Nat such that

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

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

          hence contradiction by A22;

        end;

        (s3 ^\ l) is 0 -convergent by A12, A21;

        then

        reconsider h = (s3 ^\ l) as 0 -convergent non-zero Real_Sequence by A24, SEQ_1: 5;

        now

          let n;

          

          thus ((((f /* (h + c)) - (f /* c)) + (f /* c)) . n) = ((((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n)) by SEQ_1: 7

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

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

        end;

        then

         A26: (((f /* (h + c)) - (f /* c)) + (f /* c)) = (f /* (h + c)) by FUNCT_2: 63;

        now

          let n;

          

          thus ((h + c) . n) = ((((s1 - s2) + s2) ^\ l) . n) by A11, SEQM_3: 15

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

          .= (((s1 - s2) . (n + l)) + (s2 . (n + l))) by SEQ_1: 7

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

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

        end;

        

        then

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

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

        ( rng (h + c)) c= N

        proof

          let y be object;

          assume y in ( rng (h + c));

          then

          consider n such that

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

          ((h + c) . n) = ((((s1 - s2) + s2) ^\ l) . n) by A11, SEQM_3: 15

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

          .= (((s1 - s2) . (n + l)) + (s2 . (n + l))) by SEQ_1: 7

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

          .= (s1 . (l + n));

          then |.(((h + c) . n) - x0).| < g by A9, NAT_1: 12;

          hence thesis by A4, A28, RCOMP_1: 1;

        end;

        then

         A29: ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A1, A2, A13, Th12;

        

        then

         A30: ( lim (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c))))) = ( 0 * ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))))) by A21, SEQ_2: 15

        .= 0 ;

        now

          let n be Element of NAT ;

          

           A31: (h . n) <> 0 by A24;

          

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

          .= ((h . n) * (((h " ) . n) * (((f /* (h + c)) - (f /* c)) . n))) by SEQ_1: 8

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

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

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

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

        end;

        then

         A32: (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ((f /* (h + c)) - (f /* c)) by FUNCT_2: 63;

        then

         A33: ((f /* (h + c)) - (f /* c)) is convergent by A29;

        then

         A34: (((f /* (h + c)) - (f /* c)) + (f /* c)) is convergent by A20;

        hence (f /* s1) is convergent by A27, SEQ_4: 21;

        ( lim (f /* c)) = (f . x0) by A17, A20, SEQ_2:def 7;

        

        then ( lim (((f /* (h + c)) - (f /* c)) + (f /* c))) = ( 0 + (f . x0)) by A30, A32, A33, A20, SEQ_2: 6

        .= (f . x0);

        hence (f . x0) = ( lim (f /* s1)) by A34, A27, SEQ_4: 22;

      end;

      hence thesis by FCONT_1: 2;

    end;

    theorem :: FDIFF_1:25

    f is_differentiable_on X implies (f | X) is continuous

    proof

      assume

       A1: f is_differentiable_on X;

      let x be Real;

      assume x in ( dom (f | X));

      then x is Real & x in X;

      then (f | X) is_differentiable_in x by A1;

      hence thesis by Th24;

    end;

    theorem :: FDIFF_1:26

    

     Th26: f is_differentiable_on X & Z c= X implies f is_differentiable_on Z

    proof

      assume that

       A1: f is_differentiable_on X and

       A2: Z c= X;

      X c= ( dom f) by A1;

      hence Z c= ( dom f) by A2;

      let x0;

      assume

       A3: x0 in Z;

      then (f | X) is_differentiable_in x0 by A1, A2;

      then

      consider N be Neighbourhood of x0 such that

       A4: N c= ( dom (f | X)) and

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

      consider N1 be Neighbourhood of x0 such that

       A6: N1 c= Z by A3, RCOMP_1: 18;

      consider N2 be Neighbourhood of x0 such that

       A7: N2 c= N and

       A8: N2 c= N1 by RCOMP_1: 17;

      

       A9: N2 c= Z by A6, A8;

      take N2;

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

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

      then N c= ( dom f) by A4;

      then N2 c= ( dom f) by A7;

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

      hence

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

      consider L, R such that

       A11: for x st x in N holds (((f | X) . x) - ((f | X) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A5;

      take L, R;

      let x;

      assume

       A12: x in N2;

      then (((f | X) . x) - ((f | X) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A7, A11;

      then

       A13: (((f | X) . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A2, A3, FUNCT_1: 49;

      x in N by A7, A12;

      then ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A4, A13, FUNCT_1: 47;

      then ((f . x) - ((f | Z) . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A3, FUNCT_1: 49;

      hence thesis by A10, A12, FUNCT_1: 47;

    end;

    theorem :: FDIFF_1:27

    ex R st (R . 0 ) = 0 & R is_continuous_in 0

    proof

      

       A1: ( {} REAL ) is closed by XBOOLE_1: 3;

      (( [#] REAL ) ` ) = ( {} REAL ) & REAL c= REAL & ( [#] REAL ) = REAL by XBOOLE_1: 37;

      then

      reconsider Z = ( [#] REAL ) as open Subset of REAL by A1, RCOMP_1:def 5;

      reconsider cf = ( REAL --> ( In ( 0 , REAL ))) as Function of REAL , REAL ;

      set R = cf;

      reconsider f = R as PartFunc of REAL , REAL ;

      now

        let h;

         A3:

        now

          let n be Nat;

          

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

          

           A6: n in NAT by ORDINAL1:def 12;

          

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

          .= (((h " ) . n) * (R . (h . n))) by A6, A4, FUNCT_2: 108

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

          .= 0 ;

        end;

        then

         A7: ((h " ) (#) (R /* h)) is constant by VALUED_0:def 18;

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

        (((h " ) (#) (R /* h)) . 0 ) = 0 by A3;

        hence ( lim ((h " ) (#) (R /* h))) = 0 by A7, SEQ_4: 25;

      end;

      then

      reconsider R as RestFunc by Def2;

      set L = cf;

      for p holds (L . p) = ( 0 * p);

      then

      reconsider L as LinearFunc by Def3;

      (f | Z) is constant;

      then

      consider r be Element of REAL such that

       A8: for x be Element of REAL st x in (Z /\ ( dom f)) holds (f . x) = r by PARTFUN2: 57;

       A9:

      now

        let x0;

        reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;

        assume x0 in Z;

        set N = the Neighbourhood of x0;

        

         A11: xx0 in (Z /\ ( dom f));

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

        proof

          let x;

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

          assume x in N;

          then x in (Z /\ ( dom f));

          

          hence ((f . x) - (f . x0)) = (r - (f . x0)) by A8

          .= (r - r) by A8, A11

          .= ((L . (xx - xx0)) + 0 )

          .= ((L . (x - x0)) + (R . (x - x0)));

        end;

        hence f is_differentiable_in x0;

      end;

      set x0 = the Element of REAL ;

      f is_differentiable_in x0 by A9;

      then

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

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

      consider L, R such that

       A13: for x st x in N holds ((f . x) - (f . x0)) = ((L . (x - x0)) + (R . (x - x0))) by A12;

      take R;

      consider p such that

       A14: for r holds (L . r) = (p * r) by Def3;

      ((f . x0) - (f . x0)) = ((L . (x0 - x0)) + (R . (x0 - x0))) by A13, RCOMP_1: 16;

      then

       A15: 0 = ((p * 0 ) + (R . 0 )) by A14;

      hence (R . 0 ) = 0 ;

       A16:

      now

        set s3 = cs;

        let h;

        

         A17: (s3 . 1) = 0 ;

        ((h " ) (#) (R /* h)) is convergent by Def2;

        then ((h " ) (#) (R /* h)) is bounded;

        then

        consider M be Real such that M > 0 and

         A18: for n be Nat holds |.(((h " ) (#) (R /* h)) . n).| < M by SEQ_2: 3;

         A19:

        now

          let n be Nat;

           |.(((h " ) (#) (R /* h)) . n).| = |.(((h " ) . n) * ((R /* h) . n)).| by SEQ_1: 8

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

          then

           A20: |.(((h . n) " ) * ((R /* h) . n)).| <= M by A18;

           0 <= |.((R /* h) . n).| by COMPLEX1: 46;

          then 0 <= (( abs (R /* h)) . n) by SEQ_1: 12;

          hence (s3 . n) <= (( abs (R /* h)) . n);

           |.(h . n).| >= 0 by COMPLEX1: 46;

          then ( |.(h . n).| * |.(((h . n) " ) * ((R /* h) . n)).|) <= (M * |.(h . n).|) by A20, XREAL_1: 64;

          then |.((h . n) * (((h . n) " ) * ((R /* h) . n))).| <= (M * |.(h . n).|) by COMPLEX1: 65;

          then

           A21: |.(((h . n) * ((h . n) " )) * ((R /* h) . n)).| <= (M * |.(h . n).|);

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

          then |.(1 * ((R /* h) . n)).| <= (M * |.(h . n).|) by A21, XCMPLX_0:def 7;

          then |.((R /* h) . n).| <= (M * (( abs h) . n)) by SEQ_1: 12;

          then |.((R /* h) . n).| <= ((M (#) ( abs h)) . n) by SEQ_1: 9;

          hence (( abs (R /* h)) . n) <= ((M (#) ( abs h)) . n) by SEQ_1: 12;

        end;

        ( lim h) = 0 ;

        

        then ( lim ( abs h)) = |. 0 .| by SEQ_4: 14

        .= 0 by ABSVALUE: 2;

        

        then

         A22: ( lim (M (#) ( abs h))) = (M * 0 ) by SEQ_2: 8

        .= ( lim s3) by A17, SEQ_4: 25;

        

         A23: ( abs (R /* h)) is convergent by A22, A19, SEQ_2: 19;

        ( lim s3) = 0 by A17, SEQ_4: 25;

        then ( lim ( abs (R /* h))) = 0 by A22, A19, SEQ_2: 20;

        hence (R /* h) is convergent & ( lim (R /* h)) = (R . 0 ) by A15, A23, SEQ_4: 15;

      end;

      now

        let s1;

        assume that ( rng s1) c= ( dom R) and

         A24: s1 is convergent & ( lim s1) = 0 and

         A25: for n be Nat holds (s1 . n) <> 0 ;

        s1 is 0 -convergent by A24;

        then s1 is 0 -convergent non-zero Real_Sequence by A25, SEQ_1: 5;

        hence (R /* s1) is convergent & ( lim (R /* s1)) = (R . 0 ) by A16;

      end;

      hence thesis by FCONT_1: 2;

    end;

    definition

      let f be PartFunc of REAL , REAL ;

      :: FDIFF_1:def8

      attr f is differentiable means

      : Def8: f is_differentiable_on ( dom f);

    end

    

     Lm1: ( {} REAL ) is closed by XBOOLE_1: 3;

    

     Lm2: ( [#] REAL ) is open by XBOOLE_1: 37, Lm1;

    registration

      cluster differentiable for Function of REAL , REAL ;

      existence

      proof

        reconsider Z = REAL as open Subset of REAL by Lm2;

        reconsider f = ( id REAL ) as Function of REAL , REAL ;

        take f;

        

         A1: Z = ( dom f);

        f is_differentiable_on Z by A1, Th17;

        hence thesis;

      end;

    end

    theorem :: FDIFF_1:28

    for f be differentiable PartFunc of REAL , REAL st Z c= ( dom f) holds f is_differentiable_on Z by Th26, Def8;