ndiff_3.miz

    begin

    reserve F for RealNormSpace;

    reserve G for RealNormSpace;

    reserve X for set;

    reserve x,x0,g,r,s,p 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 seq for sequence of G;

    reserve f,f1,f2 for PartFunc of REAL , the carrier of F;

    reserve h for 0 -convergent non-zero Real_Sequence;

    reserve c for constant Real_Sequence;

    set cs = ( seq_const 0 );

    theorem :: NDIFF_3:1



     Th1: (for n holds ||.(seq . n).|| <= (s1 . n)) & s1 is convergent & ( lim s1) = 0 implies seq is convergent & ( lim seq) = ( 0. G)

    proof

      assume that

       A1: for n holds ||.(seq . n).|| <= (s1 . n) and

       A2: s1 is convergent and

       A3: ( lim s1) = 0 ;

      now

        let p be Real;

        assume 0 < p;

        then

        consider n be Nat such that

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

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

        now

          let m be Nat;



           A5: m in NAT by ORDINAL1:def 12;

          assume n <= m;

          then

           A6: |.((s1 . m) - 0 ).| < p by A4;



           A7: ||.((seq . m) - ( 0. G)).|| = ||.(seq . m).|| by RLVECT_1: 13;



           A8: (s1 . m) <= |.(s1 . m).| by ABSVALUE: 4;

           ||.(seq . m).|| <= (s1 . m) by A1, A5;

          then ||.((seq . m) - ( 0. G)).|| <= |.(s1 . m).| by A7, A8, XXREAL_0: 2;

          hence ||.((seq . m) - ( 0. G)).|| < p by A6, XXREAL_0: 2;

        end;

        hence ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - ( 0. G)).|| < p;

      end;

      then

       A9: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds ||.((seq . m) - ( 0. G)).|| < p;

      hence seq is convergent by NORMSP_1:def 6;

      hence thesis by A9, NORMSP_1:def 7;

    end;

    theorem :: NDIFF_3:2



     Th2: ((s1 ^\ k) (#) (seq ^\ k)) = ((s1 (#) seq) ^\ k)

    proof

      now

        let n;



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

        .= ((s1 . (n + k)) * (seq . (n + k))) by NDIFF_1:def 2

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

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

        .= (((s1 ^\ k) (#) (seq ^\ k)) . n) by NDIFF_1:def 2;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    definition

      let F;

      let IT be PartFunc of REAL , the carrier of F;

      :: NDIFF_3:def1

      attr IT is RestFunc-like means

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

    end

    registration

      let F;

      cluster RestFunc-like for PartFunc of REAL , the carrier of F;

      existence

      proof

        take f = ( REAL --> ( 0. F));

        thus f is total;

        now

          let h;

          now

            let n be Nat;



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



             A3: n in NAT by ORDINAL1:def 12;



            thus (((h " ) (#) (f /* h)) . n) = (((h " ) . n) * ((f /* h) . n)) by NDIFF_1:def 2

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

            .= ( 0. F) by RLVECT_1: 10;

          end;

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

          hence ((h " ) (#) (f /* h)) is convergent & ( lim ((h " ) (#) (f /* h))) = ( 0. F) by NDIFF_1: 18;

        end;

        hence thesis;

      end;

    end

    definition

      let F;

      mode RestFunc of F is RestFunc-like PartFunc of REAL , the carrier of F;

    end

    definition

      let F;

      let IT be Function of REAL , the carrier of F;

      :: NDIFF_3:def2

      attr IT is linear means

      : Def2: ex r be Point of F st for p be Real holds (IT /. p) = (p * r);

    end

    registration

      let F;

      cluster linear for Function of REAL , the carrier of F;

      existence

      proof

        deffunc FG( Real) = ($1 * ( 0. F));

        consider f be Function of REAL , the carrier of F such that

         A1: for x be Element of REAL holds (f . x) = FG(x) from FUNCT_2:sch 4;



         A2: for x be Real holds (f /. x) = FG(x)

        proof

          let x be Real;

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

          (f /. x) = FG(x) by A1;

          hence thesis;

        end;

        take f;

        thus thesis by A2;

      end;

    end

    definition

      let F;

      mode LinearFunc of F is linear Function of REAL , the carrier of F;

    end

    reserve R,R1,R2 for RestFunc of F;

    reserve L,L1,L2 for LinearFunc of F;

    theorem :: NDIFF_3:3



     Th3: (L1 + L2) is LinearFunc of F & (L1 - L2) is LinearFunc of F

    proof

      consider g1 be Point of F such that

       A1: for p be Real holds (L1 /. p) = (p * g1) by Def2;

      consider g2 be Point of F such that

       A2: for p be Real holds (L2 /. p) = (p * g2) by Def2;



       A3: (L1 + L2) is total by VFUNCT_1: 32;

      now

        let p be Real;

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



        thus ((L1 + L2) /. p) = ((L1 /. pp) + (L2 /. pp)) by VFUNCT_1: 37

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

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

        .= (p * (g1 + g2)) by RLVECT_1:def 5;

      end;

      hence (L1 + L2) is LinearFunc of F by A3, Def2;



       A4: (L1 - L2) is total by VFUNCT_1: 32;

      now

        let p be Real;

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



        thus ((L1 - L2) /. p) = ((L1 /. pp) - (L2 /. pp)) by VFUNCT_1: 37

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

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

        .= (p * (g1 - g2)) by RLVECT_1: 34;

      end;

      hence thesis by A4, Def2;

    end;

    theorem :: NDIFF_3:4



     Th4: (r (#) L) is LinearFunc of F

    proof

      consider g be Point of F such that

       A1: for p be Real holds (L /. p) = (p * g) by Def2;



       A2: (r (#) L) is total by VFUNCT_1: 34;

      now

        let p be Real;

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



        thus ((r (#) L) /. p) = (r * (L /. pp)) by VFUNCT_1: 39

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

        .= ((r * p) * g) by RLVECT_1:def 7

        .= (p * (r * g)) by RLVECT_1:def 7;

      end;

      hence thesis by A2, Def2;

    end;

    theorem :: NDIFF_3:5



     Th5: for h1,h2 be PartFunc of REAL , the carrier of F holds for seq be Real_Sequence st ( rng seq) c= (( dom h1) /\ ( dom h2)) holds ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) & ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq))

    proof

      let h1,h2 be PartFunc of REAL , the carrier of F;

      let seq be Real_Sequence;



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



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

      assume

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

      then

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

      now

        let n be Nat;



         A5: n in NAT by ORDINAL1:def 12;



         A6: (seq . n) in ( rng seq) by FUNCT_2: 4, A5;



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

        .= ((h1 /. (seq . n)) + (h2 /. (seq . n))) by A4, A6, VFUNCT_1:def 1

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

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

      end;

      hence ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) by NORMSP_1:def 2;



       A7: ( rng seq) c= ( dom (h1 - h2)) by A3, VFUNCT_1:def 2;

      now

        let n be Nat;



         A8: n in NAT by ORDINAL1:def 12;



         A9: (seq . n) in ( rng seq) by FUNCT_2: 4, A8;



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

        .= ((h1 /. (seq . n)) - (h2 /. (seq . n))) by A7, A9, VFUNCT_1:def 2

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

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

      end;

      hence thesis by NORMSP_1:def 3;

    end;

    theorem :: NDIFF_3:6



     Th6: for h1,h2 be PartFunc of REAL , the carrier of F holds for seq be Real_Sequence st h1 is total & h2 is total holds ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) & ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq))

    proof

      let h1,h2 be PartFunc of REAL , the carrier of F;

      let seq be Real_Sequence;

      assume h1 is total & h2 is total;

      then (h1 + h2) is total by VFUNCT_1: 32;

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

      then (( dom h1) /\ ( dom h2)) = REAL by VFUNCT_1:def 1;

      then

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

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

      thus thesis by A1, Th5;

    end;

    theorem :: NDIFF_3:7



     Th7: (R1 + R2) is RestFunc of F & (R1 - R2) is RestFunc of F

    proof



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

       A2:

      now

        let h;



         A3: ((h " ) (#) ((R1 + R2) /* h)) = ((h " ) (#) ((R1 /* h) + (R2 /* h))) by A1, Th6

        .= (((h " ) (#) (R1 /* h)) + ((h " ) (#) (R2 /* h))) by NDIFF_1: 9;



         A4: ((h " ) (#) (R1 /* h)) is convergent & ((h " ) (#) (R2 /* h)) is convergent by Def1;

        hence ((h " ) (#) ((R1 + R2) /* h)) is convergent by A3, NORMSP_1: 19;

        ( lim ((h " ) (#) (R1 /* h))) = ( 0. F) & ( lim ((h " ) (#) (R2 /* h))) = ( 0. F) by Def1;



        hence ( lim ((h " ) (#) ((R1 + R2) /* h))) = (( 0. F) + ( 0. F)) by A4, A3, NORMSP_1: 25

        .= ( 0. F) by RLVECT_1:def 4;

      end;

      (R1 + R2) is total by A1, VFUNCT_1: 32;

      hence (R1 + R2) is RestFunc of F by A2, Def1;

       A5:

      now

        let h;



         A6: ((h " ) (#) ((R1 - R2) /* h)) = ((h " ) (#) ((R1 /* h) - (R2 /* h))) by A1, Th6

        .= (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R2 /* h))) by NDIFF_1: 12;



         A7: ((h " ) (#) (R1 /* h)) is convergent & ((h " ) (#) (R2 /* h)) is convergent by Def1;

        hence ((h " ) (#) ((R1 - R2) /* h)) is convergent by A6, NORMSP_1: 20;

        ( lim ((h " ) (#) (R1 /* h))) = ( 0. F) & ( lim ((h " ) (#) (R2 /* h))) = ( 0. F) by Def1;



        hence ( lim ((h " ) (#) ((R1 - R2) /* h))) = (( 0. F) - ( 0. F)) by A7, A6, NORMSP_1: 26

        .= ( 0. F) by RLVECT_1: 13;

      end;

      (R1 - R2) is total by A1, VFUNCT_1: 32;

      hence (R1 - R2) is RestFunc of F by A5, Def1;

    end;

    theorem :: NDIFF_3:8



     Th8: (r (#) R) is RestFunc of F

    proof



       A1: R is total by Def1;

      then

       A2: (r (#) R) is total by VFUNCT_1: 34;

      now

        let h;

        ( dom R) = REAL by A1, FUNCT_2:def 1;

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



        then

         A3: ((h " ) (#) ((r (#) R) /* h)) = ((h " ) (#) (r * (R /* h))) by NFCONT_3: 4

        .= (r * ((h " ) (#) (R /* h))) by NDIFF_1: 10;



         A4: ((h " ) (#) (R /* h)) is convergent by Def1;

        hence ((h " ) (#) ((r (#) R) /* h)) is convergent by A3, NORMSP_1: 22;

        ( lim ((h " ) (#) (R /* h))) = ( 0. F) by Def1;



        hence ( lim ((h " ) (#) ((r (#) R) /* h))) = (r * ( 0. F)) by A4, A3, NORMSP_1: 28

        .= ( 0. F) by RLVECT_1: 10;

      end;

      hence thesis by A2, Def1;

    end;

    definition

      let F, f;

      let x0 be Real;

      :: NDIFF_3:def3

      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, f;

      let x0 be Real;

      assume

       A1: f is_differentiable_in x0;

      :: NDIFF_3:def4

      func diff (f,x0) -> Point of F means

      : Def4: 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 be Point of F such that

         A5: for p be Real holds (L /. p) = (p * r) by Def2;

        take r;

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

        .= r by RLVECT_1:def 8;

        hence thesis by A2, A4;

      end;

      uniqueness

      proof

        let r,s be Point of F;

        assume that

         A6: ex N be Neighbourhood of x0 st N c= ( dom f) & ex L, R st r = (L /. 1) & for x be Real 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 be Real 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 be Real 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 be Real st x in N holds ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A8;

        consider r1 be Point of F such that

         A11: for p be Real holds (L /. p) = (p * r1) by Def2;

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

         A12: ex L, R st s = (L /. 1) & for x be Real 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 be Real st x in N1 holds ((f /. x) - (f /. x0)) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A12;

        consider p1 be Point of F such that

         A15: for p be Real holds (L1 /. p) = (p * p1) by Def2;

        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

        reconsider h = s1 as 0 -convergent non-zero Real_Sequence by A20, FDIFF_1:def 1;



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

        proof

          let n;

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

          reconsider z0 = 0 as Element of NAT ;

          (z0 + 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 = (1 * p1) by A13, A15;



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

         A25:

        now

          let x be Real;

          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 (((x - x0) * r1) + (R /. (x - x0))) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A11;

          then ((((x - x0) * 1) * r1) + (R /. (x - x0))) = ((((x - x0) * 1) * p1) + (R1 /. (x - x0))) by A15;

          then ((((x - x0) * 1) * r) + (R /. (x - x0))) = ((((x - x0) * 1) * p1) + (R1 /. (x - x0))) by A24, RLVECT_1:def 7;

          hence (((x - x0) * r) + (R /. (x - x0))) = (((x - x0) * s) + (R1 /. (x - x0))) by A23, RLVECT_1:def 7;

        end;

        now

          R1 is total by Def1;

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

          then

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

          let n be Nat;

          R is total by Def1;

          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 be Real st x in N & x in N1 & (h . n) = (x - x0) by A21;

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

          then (((1 / (h . n)) * ((h . n) * r)) + ((1 / (h . n)) * (R /. (h . n)))) = ((1 / (h . n)) * (((h . n) * s) + (R1 /. (h . n)))) by RLVECT_1:def 5;

          then ((((1 / (h . n)) * (h . n)) * r) + ((1 / (h . n)) * (R /. (h . n)))) = ((1 / (h . n)) * (((h . n) * s) + (R1 /. (h . n)))) by RLVECT_1:def 7;

          then

           A31: ((((1 / (h . n)) * (h . n)) * r) + ((1 / (h . n)) * (R /. (h . n)))) = (((1 / (h . n)) * ((h . n) * s)) + ((1 / (h . n)) * (R1 /. (h . n)))) by RLVECT_1:def 5;



           A32: ((1 / (h . n)) * (R /. (h . n))) = (((h . n) " ) * (R /. (h . n))) by XCMPLX_1: 215

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

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

          .= (((h " ) (#) (R /* h)) . n) by NDIFF_1:def 2;



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



           A34: ((1 / (h . n)) * (R1 /. (h . n))) = (((h . n) " ) * (R1 /. (h . n))) by XCMPLX_1: 215

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

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

          .= (((h " ) (#) (R1 /* h)) . n) by NDIFF_1:def 2;



           A35: (((1 / (h . n)) * (h . n)) * s) = (1 * s) by A33, XCMPLX_1: 106

          .= s by RLVECT_1:def 8;

          (((1 / (h . n)) * (h . n)) * r) = (1 * r) by A33, XCMPLX_1: 106

          .= r by RLVECT_1:def 8;

          then (r + (((h " ) (#) (R /* h)) . n)) = (s + (((h " ) (#) (R1 /* h)) . n)) by A31, A35, A32, A34, RLVECT_1:def 7;

          then (r + ((((h " ) (#) (R /* h)) . n) - (((h " ) (#) (R /* h)) . n))) = ((s + (((h " ) (#) (R1 /* h)) . n)) - (((h " ) (#) (R /* h)) . n)) by RLVECT_1: 28;

          then (r + ((((h " ) (#) (R /* h)) . n) - (((h " ) (#) (R /* h)) . n))) = (s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by RLVECT_1: 28;

          then (r + ( 0. F)) = (s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by RLVECT_1: 15;

          then r = (s + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n))) by RLVECT_1: 4;

          then (r - s) = (((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n)) + (s - s)) by RLVECT_1: 28;

          then (r - s) = (((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n)) + ( 0. F)) by RLVECT_1: 15;

          then

           A36: (r - s) = ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n)) by RLVECT_1: 4;

          thus (r - s) = ((((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n) by A36, NORMSP_1:def 3;

        end;

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

        then

         A37: ( lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)))) = (r - s) by NDIFF_1: 18;



         A38: ((h " ) (#) (R1 /* h)) is convergent & ( lim ((h " ) (#) (R1 /* h))) = ( 0. F) by Def1;

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

        then (r - s) = (( 0. F) - ( 0. F)) by A37, A38, NORMSP_1: 26;

        hence thesis by RLVECT_1: 13, RLVECT_1: 21;

      end;

    end

    definition

      let F, f, X;

      :: NDIFF_3:def5

      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 :: NDIFF_3:9



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

    theorem :: NDIFF_3:10



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

    proof

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

      proof

        assume

         A1: f is_differentiable_on Z;

        hence

         A2: Z c= ( dom f);

        let x0;

        assume

         A3: x0 in Z;

        then (f | Z) is_differentiable_in x0 by A1;

        then

        consider N be Neighbourhood of x0 such that

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

         A5: 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 A4;

        consider L, R such that

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

        now

          let x;

          assume

           A7: x in N;

          then

           A8: (((f | Z) /. x) - ((f | Z) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A6;

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

          hence ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A2, A3, PARTFUN2: 17;

        end;

        hence thesis;

      end;

      assume that

       A9: Z c= ( dom f) and

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

      thus Z c= ( dom f) by A9;

      let x0;

      assume

       A11: x0 in Z;

      then

      consider N1 be Neighbourhood of x0 such that

       A12: N1 c= Z by RCOMP_1: 18;

      f is_differentiable_in x0 by A10, A11;

      then

      consider N be Neighbourhood of x0 such that

       A13: N c= ( dom f) and

       A14: 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

       A15: N2 c= N1 and

       A16: N2 c= N by RCOMP_1: 17;



       A17: N2 c= Z by A12, A15;

      take N2;

      N2 c= ( dom f) by A13, A16;

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

      hence

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

      consider L, R such that

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



       A20: x0 in N2 by RCOMP_1: 16;

      take L, R;

      now

        let x;

        assume

         A21: x in N2;

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

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

        hence (((f | Z) /. x) - ((f | Z) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A20, A18, PARTFUN2: 15;

      end;

      hence thesis;

    end;

    theorem :: NDIFF_3:11

    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, f, X;

      assume

       A1: f is_differentiable_on X;

      :: NDIFF_3:def6

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

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

      existence

      proof

        deffunc FG( Real) = ( diff (f,$1));

        defpred P[ set] means $1 in X;

        consider F0 be PartFunc of REAL , the carrier of F such that

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

        take F0;

        now



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

          let y be object;

          assume y in X;

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

        end;

        then

         A4: X c= ( dom F0);

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

        then ( dom F0) c= X;

        hence ( dom F0) = X by A4;

        now

          let x;

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

          assume x in X;

          then xx in ( dom F0) by A2;

          hence (F0 . x) = ( diff (f,x)) by A2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let F0,G0 be PartFunc of REAL , the carrier of F;

        assume that

         A5: ( dom F0) = X and

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

         A7: ( dom G0) = X and

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

        now

          let x be Element of REAL ;

          assume

           A9: x in ( dom F0);

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

          hence (F0 . x) = (G0 . x) by A5, A8, A9;

        end;

        hence thesis by A5, A7, PARTFUN1: 5;

      end;

    end

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

    theorem :: NDIFF_3:12

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

    proof

      set R = ( REAL --> ( 0. F));



       A1: ( dom R) = REAL ;

      now

        let h;

        now

          let n be Nat;



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



           A3: n in NAT by ORDINAL1:def 12;



          thus (((h " ) (#) (R /* h)) . n) = (((h " ) . n) * ((R /* h) . n)) by NDIFF_1:def 2

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

          .= ( 0. F) by RLVECT_1: 10;

        end;

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

        hence ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = ( 0. F) by NDIFF_1: 18;

      end;

      then

      reconsider R as RestFunc of F by Def1;

      reconsider L = ( REAL --> ( 0. F)) as Function of REAL , F;

      now

        let p be Real;

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



        thus (L /. p) = (L /. pp)

        .= ( 0. F)

        .= (p * ( 0. F)) by RLVECT_1: 10;

      end;

      then

      reconsider L as LinearFunc of F by Def2;

      assume

       A4: Z c= ( dom f);

      given r be Point of F such that

       A5: ( rng f) = {r};

       A6:

      now

        let x0;

        assume

         A7: x0 in ( dom f);

        then (f /. x0) = (f . x0) by PARTFUN1:def 6;

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

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

      end;

       A8:

      now

        let x0;

        assume

         A9: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A10: N c= Z by RCOMP_1: 18;



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

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

        proof

          let x;



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



          then

           A13: (R /. (x - x0)) = (R . (x - x0)) by A1, PARTFUN1:def 6

          .= ( 0. F) by FUNCOP_1: 7, A12;

          assume x in N;



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

          .= (r - r) by A4, A6, A9

          .= ( 0. F) by RLVECT_1: 15

          .= (L . (x - x0)) by FUNCOP_1: 7, A12

          .= (L /. (x - x0)) by A1, PARTFUN1:def 6, A12

          .= ((L /. (x - x0)) + (R /. (x - x0))) by A13, RLVECT_1: 4;

        end;

        hence f is_differentiable_in x0 by A11;

      end;

      hence

       A14: f is_differentiable_on Z by A4, Th10;

      let x0;

      assume

       A15: x0 in Z;

      then

       A16: f is_differentiable_in x0 by A8;

      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;



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



        then

         A20: (R /. (x - x0)) = (R . (x - x0)) by A1, PARTFUN1:def 6

        .= ( 0. F) by FUNCOP_1: 7, A19;

        assume x in N;



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

        .= (r - r) by A4, A6, A15

        .= ( 0. F) by RLVECT_1: 15

        .= (L . (x - x0)) by FUNCOP_1: 7, A19

        .= (L /. (x - x0)) by A1, PARTFUN1:def 6, A19

        .= ((L /. (x - x0)) + (R /. (x - x0))) by A20, RLVECT_1: 4;

      end;

      ( dom (f `| Z)) = Z by A14, Def6;



      hence ((f `| Z) /. x0) = ((f `| Z) . x0) by A15, PARTFUN1:def 6

      .= ( diff (f,x0)) by A14, A15, Def6

      .= (L /. jj) by A16, A17, A18, Def4

      .= ( 0. F);

    end;

    theorem :: NDIFF_3:13



     Th13: 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;

      reconsider z0 = 0 as Nat;

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

      then

       A11: x0 in N2 by A10;

      now

        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 y in ( dom f) by A2;

      end;

      then

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

      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;

        reconsider z0 = 0 as Real;

        ( lim h) = z0;



        then ( lim (h + c)) = (z0 + 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;

        for y be object st y in ( rng (c ^\ n)) holds y in N2 by A11, A15, TARSKI:def 1;

        hence ( rng (c ^\ n)) c= N2;

        now

          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;

          reconsider z0 = 0 as Nat;

          (n + z0) <= (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 y in N2 by A10, A16, A18;

        end;

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

      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;

      now

        let y be object;

        assume

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

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

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

        then y in N by A4, A11;

        hence y in ( dom f) by A2;

      end;

      then

       A22: ( rng (c ^\ n)) c= ( dom f);



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

      proof

        deffunc F0( Element of NAT ) = ((L . jj) + ((((h ^\ n) " ) (#) (R /* (h ^\ n))) . $1));

        consider s1 be sequence of the carrier of F such that

         A24: for k holds (s1 . k) = F0(k) from FUNCT_2:sch 4;

         A25:

        now



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

          let r be Real;

          assume 0 < r;

          then

          consider m be Nat such that

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

          take n1 = m;

          let k be Nat such that

           A28: n1 <= k;



           A29: k in NAT by ORDINAL1:def 12;



           A30: ||.((s1 . k) - (L /. jj)).|| = ||.(((L . jj) + ((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k)) - (L /. jj)).|| by A24, A29

          .= ||.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) + ((L /. jj) - (L /. jj))).|| by RLVECT_1: 28

          .= ||.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) + ( 0. F)).|| by RLVECT_1: 15

          .= ||.((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k).|| by RLVECT_1: 4;

           ||.(((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - ( 0. F)).|| < r by A27, A28;

          hence ||.((s1 . k) - (L /. jj)).|| < r by A30, RLVECT_1: 13;

        end;

        consider s be Point of F such that

         A31: for p1 be Real holds (L /. p1) = (p1 * s) by Def2;



         A32: (L /. jj) = (1 * s) by A31

        .= s by RLVECT_1:def 8;

        now

          let m;



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



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

          .= (((((h ^\ n) " ) (#) (L /* (h ^\ n))) . m) + ((((h ^\ n) " ) (#) (R /* (h ^\ n))) . m)) by NORMSP_1:def 2

          .= (((((h ^\ n) " ) . m) * ((L /* (h ^\ n)) . m)) + ((((h ^\ n) " ) (#) (R /* (h ^\ n))) . m)) by NDIFF_1:def 2

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

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

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

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

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

          .= (s + ((((h ^\ n) " ) (#) (R /* (h ^\ n))) . m)) by RLVECT_1:def 8

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

        end;

        then

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

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

        hence thesis by A34, A25, NORMSP_1:def 7;

      end;

      for y be object st y in ( rng ((h + c) ^\ n)) holds y in ( dom f) by A2, A4, A19;

      then

       A35: ( rng ((h + c) ^\ n)) c= ( dom f);

      for y be object st y in ( rng (h + c)) holds y in ( dom f) by A2, A8;

      then

       A36: ( rng (h + c)) c= ( dom f);



       A37: 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

         A38: (((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

         A39: ((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, A38, A39;

      end;



       A40: R is total by Def1;

      now

        let k;

        ( dom R) = REAL by A40, FUNCT_2:def 1;

        then

         A41: ( rng (h ^\ n)) c= ( dom R);



        thus (((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k) = (((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k)) by NORMSP_1:def 3

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

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

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

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

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

        .= (((L /* (h ^\ n)) + (R /* (h ^\ n))) . k) by NORMSP_1:def 2;

      end;

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



      then

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

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

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

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

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

      then

       A43: (L /. 1) = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) by A23, LOPBAN_3: 11;

      thus ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A23, A42, LOPBAN_3: 10;

      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, A43, Def4;

    end;

    theorem :: NDIFF_3: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

      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 of F by Th7;

      reconsider L = (L1 + L2) as LinearFunc of F by Th3;

      consider N be Neighbourhood of x0 such that

       A9: N c= N1 and

       A10: N c= N2 by RCOMP_1: 17;



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

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

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

      then

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

      R1 is total & R2 is total by Def1;

      then (R1 + R2) is total by VFUNCT_1: 32;

      then

       A13: ( dom (R1 + R2)) = REAL by FUNCT_2:def 1;

      (L1 + L2) is total by VFUNCT_1: 32;

      then

       A14: ( dom (L1 + L2)) = REAL by FUNCT_2:def 1;

       A15:

      now

        let x;



         A16: x0 in N by RCOMP_1: 16;



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

        assume

         A18: x in N;



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

        .= (((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0))) by A12, A16, VFUNCT_1:def 1

        .= ((f1 /. x) + ((f2 /. x) - ((f1 /. x0) + (f2 /. x0)))) by RLVECT_1: 28

        .= ((f1 /. x) + (((f2 /. x) - (f2 /. x0)) - (f1 /. x0))) by RLVECT_1: 27

        .= (((f1 /. x) + ((f2 /. x) - (f2 /. x0))) - (f1 /. x0)) by RLVECT_1: 28

        .= (((f2 /. x) - (f2 /. x0)) + ((f1 /. x) - (f1 /. x0))) by RLVECT_1: 28

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

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

        .= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (L2 /. (x - x0))) + (R2 /. (x - x0))) by RLVECT_1:def 3

        .= ((((L1 /. (x - x0)) + (L2 /. (x - x0))) + (R1 /. (x - x0))) + (R2 /. (x - x0))) by RLVECT_1:def 3

        .= (((L1 /. (x - x0)) + (L2 /. (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0)))) by RLVECT_1:def 3

        .= ((L /. (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0)))) by A14, VFUNCT_1:def 1, A17

        .= ((L /. (x - x0)) + (R /. (x - x0))) by A13, VFUNCT_1:def 1, A17;

      end;

      hence (f1 + f2) is_differentiable_in x0 by A12;



      hence ( diff ((f1 + f2),x0)) = (L /. jj) by A12, A15, Def4

      .= (L /. jj)

      .= ((L1 /. jj) + (L2 /. jj)) by A14, VFUNCT_1:def 1

      .= ((L1 /. jj) + (L2 /. jj))

      .= ((L1 /. jj) + (L2 /. jj))

      .= (( diff (f1,x0)) + (L2 /. jj)) by A1, A3, A5, Def4

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

    end;

    theorem :: NDIFF_3:15



     Th15: 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

      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 of F by Th7;

      reconsider L = (L1 - L2) as LinearFunc of F by Th3;

      consider N be Neighbourhood of x0 such that

       A9: N c= N1 and

       A10: N c= N2 by RCOMP_1: 17;



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

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

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

      then

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

      R1 is total & R2 is total by Def1;

      then (R1 - R2) is total by VFUNCT_1: 32;

      then

       A13: ( dom (R1 - R2)) = REAL by FUNCT_2:def 1;

      (L1 - L2) is total by VFUNCT_1: 32;

      then

       A14: ( dom (L1 - L2)) = REAL by FUNCT_2:def 1;

       A15:

      now

        let x;



         A16: x0 in N by RCOMP_1: 16;



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

        assume

         A18: x in N;



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

        .= (((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0))) by A12, A16, VFUNCT_1:def 2

        .= ((f1 /. x) - ((f2 /. x) + ((f1 /. x0) - (f2 /. x0)))) by RLVECT_1: 27

        .= ((f1 /. x) - (((f2 /. x) + (f1 /. x0)) - (f2 /. x0))) by RLVECT_1: 28

        .= ((f1 /. x) - ((f1 /. x0) + ((f2 /. x) - (f2 /. x0)))) by RLVECT_1: 28

        .= (((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0))) by RLVECT_1: 27

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

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

        .= ((L1 /. (x - x0)) + ((R1 /. (x - x0)) - ((L2 /. (x - x0)) + (R2 /. (x - x0))))) by RLVECT_1: 28

        .= ((L1 /. (x - x0)) + (((R1 /. (x - x0)) - (R2 /. (x - x0))) - (L2 /. (x - x0)))) by RLVECT_1: 27

        .= (((L1 /. (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))) - (L2 /. (x - x0))) by RLVECT_1: 28

        .= (((L1 /. (x - x0)) - (L2 /. (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))) by RLVECT_1: 28

        .= ((L /. (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))) by A14, VFUNCT_1:def 2, A17

        .= ((L /. (x - x0)) + (R /. (x - x0))) by A13, VFUNCT_1:def 2, A17;

      end;

      hence (f1 - f2) is_differentiable_in x0 by A12;



      hence ( diff ((f1 - f2),x0)) = (L /. jj) by A12, A15, Def4

      .= (L /. jj)

      .= ((L1 /. jj) - (L2 /. jj)) by A14, VFUNCT_1:def 2

      .= ((L1 /. jj) - (L2 /. jj))

      .= ((L1 /. jj) - (L2 /. jj))

      .= (( diff (f1,x0)) - (L2 /. jj)) by A1, A3, A5, Def4

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

    end;

    theorem :: NDIFF_3:16



     Th16: for r be Real st f is_differentiable_in x0 holds (r (#) f) is_differentiable_in x0 & ( diff ((r (#) f),x0)) = (r * ( diff (f,x0)))

    proof

      let r be Real;

      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 of F by Th8;

      reconsider L = (r (#) L1) as LinearFunc of F by Th4;



       A5: N1 c= ( dom (r (#) f)) by A2, VFUNCT_1:def 4;

      R1 is total by Def1;

      then (r (#) R1) is total by VFUNCT_1: 34;

      then

       A6: ( dom (r (#) R1)) = REAL by FUNCT_2:def 1;

      (r (#) L1) is total by VFUNCT_1: 34;

      then

       A7: ( dom (r (#) L1)) = REAL by FUNCT_2:def 1;

       A8:

      now

        let x;



         A9: x0 in N1 by RCOMP_1: 16;



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

        assume

         A11: x in N1;



        hence (((r (#) f) /. x) - ((r (#) f) /. x0)) = ((r * (f /. x)) - ((r (#) f) /. x0)) by A5, VFUNCT_1:def 4

        .= ((r * (f /. x)) - (r * (f /. x0))) by A5, A9, VFUNCT_1:def 4

        .= (r * ((f /. x) - (f /. x0))) by RLVECT_1: 34

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

        .= ((r * (L1 /. (x - x0))) + (r * (R1 /. (x - x0)))) by RLVECT_1:def 5

        .= ((L /. (x - x0)) + (r * (R1 /. (x - x0)))) by A7, VFUNCT_1:def 4, A10

        .= ((L /. (x - x0)) + (R /. (x - x0))) by A6, VFUNCT_1:def 4, A10;

      end;

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



      hence ( diff ((r (#) f),x0)) = (L /. jj) by A5, A8, Def4

      .= (L /. jj)

      .= (r * (L1 /. jj)) by A7, VFUNCT_1:def 4

      .= (r * (L1 /. jj))

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

    end;

    theorem :: NDIFF_3:17

    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, Th10;

        hence (f1 + f2) is_differentiable_in x0 by Th14;

      end;

      hence

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

      let x;

      assume

       A4: x in Z;

      then

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



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

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

    end;

    theorem :: NDIFF_3: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, Th10;

        hence (f1 - f2) is_differentiable_in x0 by Th15;

      end;

      hence

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

      let x;

      assume

       A4: x in Z;

      then

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



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

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

    end;

    theorem :: NDIFF_3:19

    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, Th10;

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

      end;

      hence

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

      let x;

      assume

       A4: x in Z;

      then

       A5: f is_differentiable_in x by A2, Th10;



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

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

    end;

    theorem :: NDIFF_3:20

    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. F)

    proof

      set R = ( REAL --> ( 0. F));



       A1: ( dom R) = REAL ;

      now

        let h;

        now

          let n be Nat;



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



           A3: n in NAT by ORDINAL1:def 12;



          thus (((h " ) (#) (R /* h)) . n) = (((h " ) . n) * ((R /* h) . n)) by NDIFF_1:def 2

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

          .= ( 0. F) by RLVECT_1: 10;

        end;

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

        hence ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = ( 0. F) by NDIFF_1: 18;

      end;

      then

      reconsider R as RestFunc of F by Def1;

      set L = ( REAL --> ( 0. F));

      now

        let p be Real;

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



        thus (L /. p) = (L /. pp)

        .= ( 0. F)

        .= (p * ( 0. F)) by RLVECT_1: 10;

      end;

      then

      reconsider L as LinearFunc of F by Def2;

      assume that

       A4: Z c= ( dom f) and

       A5: (f | Z) is constant;

      consider r be Point of F such that

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

       A7:

      now

        let x;

        assume

         A8: x in (Z /\ ( dom f));

        then x in ( dom f) by XBOOLE_0:def 4;



        hence (f /. x) = (f . x) by PARTFUN1:def 6

        .= r by A8, A6;

      end;

       A9:

      now

        let x0;

        assume

         A10: x0 in Z;

        then

        consider N be Neighbourhood of x0 such that

         A11: N c= Z by RCOMP_1: 18;



         A12: N c= ( dom f) by A4, A11;



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

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

        proof

          let x;



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



          then

           A15: (R /. (x - x0)) = (R . (x - x0)) by A1, PARTFUN1:def 6

          .= ( 0. F) by FUNCOP_1: 7, A14;

          assume x in N;

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



          hence ((f /. x) - (f /. x0)) = (r - (f /. x0)) by A7

          .= (r - r) by A7, A13

          .= ( 0. F) by RLVECT_1: 15

          .= (L . (x - x0)) by FUNCOP_1: 7, A14

          .= (L /. (x - x0)) by A1, PARTFUN1:def 6, A14

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

        end;

        hence f is_differentiable_in x0 by A12;

      end;

      hence

       A16: f is_differentiable_on Z by A4, Th10;

      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: N c= ( dom f) by A4, A18;



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



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

      proof

        let x;



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



        then

         A23: (R /. (x - x0)) = (R . (x - x0)) by A1, PARTFUN1:def 6

        .= ( 0. F) by FUNCOP_1: 7, A22;

        assume x in N;

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



        hence ((f /. x) - (f /. x0)) = (r - (f /. x0)) by A7

        .= (r - r) by A7, A20

        .= ( 0. F) by RLVECT_1: 15

        .= (L . (x - x0)) by FUNCOP_1: 7, A22

        .= (L /. (x - x0)) by A1, PARTFUN1:def 6, A22

        .= ((L /. (x - x0)) + (R /. (x - x0))) by A23, RLVECT_1: 4;

      end;



       A24: f is_differentiable_in x0 by A9, A17;



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

      .= (L /. jj) by A24, A19, A21, Def4

      .= ( 0. F);

    end;

    theorem :: NDIFF_3:21



     Th21: for r,p be Point of F, Z, f st Z c= ( dom f) & (for x st x in Z holds (f /. x) = ((x * r) + p)) holds f is_differentiable_on Z & for x st x in Z holds ((f `| Z) . x) = r

    proof

      let r,p be Point of F;

      let Z, f;

      set R = ( REAL --> ( 0. F));

      defpred P[ object] means $1 in REAL ;



       A1: ( dom R) = REAL ;

      now

        let h;

        now

          let n be Nat;



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



           A3: n in NAT by ORDINAL1:def 12;



          thus (((h " ) (#) (R /* h)) . n) = (((h " ) . n) * ((R /* h) . n)) by NDIFF_1:def 2

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

          .= ( 0. F) by RLVECT_1: 10;

        end;

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

        hence ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = ( 0. F) by NDIFF_1: 18;

      end;

      then

      reconsider R as RestFunc of F by Def1;

      assume that

       A4: Z c= ( dom f) and

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

      deffunc G( Real) = ($1 * r);

      consider L be PartFunc of REAL , the carrier of F such that

       A6: (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 x be Real holds x in ( dom L) iff P[x] by A6;

      then

       A7: ( dom L) = REAL by FDIFF_1: 1;



       A8: for x be Element of REAL holds (L /. x) = G(x)

      proof

        let x be Element of REAL ;



         A9: x in ( dom L) by A7;

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

        hence thesis by PARTFUN1:def 6, A9;

      end;



       A10: L is total by PARTFUN1:def 2, A7;

       A11:

      now

        let x;

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



        thus (L /. x) = (L /. xx)

        .= (x * r) by A8;

      end;

      then

      reconsider L as LinearFunc of F by A10, Def2;

       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 be Real;



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



          then

           A17: (R /. (x - x0)) = (R . (x - x0)) by A1, PARTFUN1:def 6

          .= ( 0. F) by FUNCOP_1: 7, A16;

          assume x in N;



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

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

          .= ((((x * r) + p) - (x0 * r)) - p) by RLVECT_1: 27

          .= ((p + ((x * r) - (x0 * r))) - p) by RLVECT_1: 28

          .= (((x * r) - (x0 * r)) + (p - p)) by RLVECT_1: 28

          .= (((x * r) - (x0 * r)) + ( 0. F)) by RLVECT_1: 15

          .= (((x - x0) * r) + ( 0. F)) by RLVECT_1: 35

          .= ((L /. (x - x0)) + (R /. (x - x0))) by A17, A11;

        end;

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

        hence f is_differentiable_in x0 by A15;

      end;

      hence

       A18: f is_differentiable_on Z by A4, Th10;

      let x0;

      assume

       A19: x0 in Z;

      then

      consider N be Neighbourhood of x0 such that

       A20: N c= Z by RCOMP_1: 18;



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

      proof

        let x;



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



        then

         A23: (R /. (x - x0)) = (R . (x - x0)) by A1, PARTFUN1:def 6

        .= ( 0. F) by FUNCOP_1: 7, A22;

        assume x in N;



        hence ((f /. x) - (f /. x0)) = (((x * r) + p) - (f /. x0)) by A5, A20

        .= (((x * r) + p) - ((x0 * r) + p)) by A5, A19

        .= ((((x * r) + p) - (x0 * r)) - p) by RLVECT_1: 27

        .= ((p + ((x * r) - (x0 * r))) - p) by RLVECT_1: 28

        .= (((x * r) - (x0 * r)) + (p - p)) by RLVECT_1: 28

        .= (((x * r) - (x0 * r)) + ( 0. F)) by RLVECT_1: 15

        .= (((x - x0) * r) + ( 0. F)) by RLVECT_1: 35

        .= ((L /. (x - x0)) + (R /. (x - x0))) by A23, A11;

      end;



       A24: N c= ( dom f) by A4, A20;



       A25: f is_differentiable_in x0 by A12, A19;



      thus ((f `| Z) . x0) = ( diff (f,x0)) by A18, A19, Def6

      .= (L /. jj) by A25, A24, A21, Def4

      .= (1 * r) by A11

      .= r by RLVECT_1:def 8;

    end;

    theorem :: NDIFF_3:22



     Th22: for x0 be Real st f is_differentiable_in x0 holds 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)));



       A3: x0 in N by RCOMP_1: 16;

      now

        consider g be Real such that

         A4: 0 < g and

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

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

        set s2 = ( seq_const x0);

        let s1 such that

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

         A7: s1 is convergent and

         A8: ( lim s1) = x0 and

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

        consider l be Nat such that

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

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

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

        consider s3 such that

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



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

        then

         A13: s3 is convergent by A7;



         A14: ( rng c) = {x0}

        proof

          thus ( rng c) c= {x0}

          proof

            let y be object;

            assume y in ( rng c);

            then

            consider n such that

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

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

            then y = x0 by SEQ_1: 57;

            hence y in {x0} by TARSKI:def 1;

          end;

          let y be object;

          assume y in {x0};

          then

           A16: y = x0 by TARSKI:def 1;

          reconsider z0 = 0 as Element of NAT ;

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

          .= y by A16, SEQ_1: 57;

          hence y in ( rng c) 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, A14, ZFMISC_1: 31;



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

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

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

          .= ||.( 0. F).|| by RLVECT_1: 15

          .= 0 ;

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

        end;

        then

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

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

        .= x0 by SEQ_1: 57;



        then ( lim s3) = (x0 - x0) by A7, A8, A12, SEQ_2: 12

        .= 0 ;

        then

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

         A22:

        now

          given n such that

           A23: (s3 . n) = 0 ;

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

          hence contradiction by A9, SEQ_1: 57;

        end;

         A24:

        now

          given n be Nat such that

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



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

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

          hence contradiction by A22, A26;

        end;

        then (s3 ^\ l) is non-zero by SEQ_1: 5;

        then

        reconsider h = (s3 ^\ l) as 0 -convergent non-zero Real_Sequence by A13, A21, FDIFF_1:def 1;

        now

          let n;



          thus ((((f /* (h + c)) - (f /* c)) + (f /* c)) . n) = ((((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n)) by NORMSP_1:def 2

          .= ((((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n)) by NORMSP_1:def 3

          .= (((f /* (h + c)) . n) - (((f /* c) . n) - ((f /* c) . n))) by RLVECT_1: 29

          .= (((f /* (h + c)) . n) - ( 0. F)) by RLVECT_1: 15

          .= ((f /* (h + c)) . n) by RLVECT_1: 13;

        end;

        then

         A27: (((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 A12, 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

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

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

        now

          let y be object;

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

          then

          consider n such that

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

          ((h + c) . n) = ((((s1 - s2) + s2) ^\ l) . n) by A12, 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 A10, NAT_1: 12;

          hence y in N by A5, A29, RCOMP_1: 1;

        end;

        then

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



         A31: ( lim (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c))))) = ( 0 * ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))))) by A21, A1, A2, A14, Th13, A30, NDIFF_1: 14

        .= ( 0. F) by RLVECT_1: 10;

        now

          let n;



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



          thus ((h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) . n) = ((h . n) * (((h " ) (#) ((f /* (h + c)) - (f /* c))) . n)) by NDIFF_1:def 2

          .= ((h . n) * (((h " ) . n) * (((f /* (h + c)) - (f /* c)) . n))) by NDIFF_1:def 2

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

          .= (((h . n) * ((h . n) " )) * (((f /* (h + c)) - (f /* c)) . n)) by RLVECT_1:def 7

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

          .= (((f /* (h + c)) - (f /* c)) . n) by RLVECT_1:def 8;

        end;

        then

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

        then

         A34: ((f /* (h + c)) - (f /* c)) is convergent by A30, A1, A2, A14, Th13, NDIFF_1: 13;

        then (((f /* (h + c)) - (f /* c)) + (f /* c)) is convergent by A20, NORMSP_1: 19;

        hence (f /* s1) is convergent by A28, LOPBAN_3: 10;

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



        then ( lim (((f /* (h + c)) - (f /* c)) + (f /* c))) = (( 0. F) + (f /. x0)) by A31, A33, A34, A20, NORMSP_1: 25

        .= (f /. x0) by RLVECT_1: 4;

        hence (f /. x0) = ( lim (f /* s1)) by A34, A28, A20, LOPBAN_3: 11, NORMSP_1: 19;

      end;

      hence thesis by A3, A2, NFCONT_3: 7;

    end;

    theorem :: NDIFF_3:23

    f is_differentiable_on X implies (f | X) is continuous

    proof

      assume

       A1: f is_differentiable_on X;

      for x be Real st x in ( dom (f | X)) holds (f | X) is_continuous_in x by A1, Th22;

      hence thesis by NFCONT_3:def 2;

    end;

    theorem :: NDIFF_3:24



     Th24: 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;

      then

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

      now

        let x0;

        assume

         A4: x0 in Z;

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

        then

        consider N be Neighbourhood of x0 such that

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

         A6: 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

         A7: N1 c= Z by A4, RCOMP_1: 18;

        consider N2 be Neighbourhood of x0 such that

         A8: N2 c= N and

         A9: N2 c= N1 by RCOMP_1: 17;



         A10: N2 c= Z by A7, A9;

        ( 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 A5;

        then N2 c= ( dom f) by A8;

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

        then

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



         A12: N2 c= ( dom (f | X)) by A8, A5;

        consider L, R such that

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

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

        proof

          let x;

          assume

           A14: x in N2;

          then

           A15: (((f | X) /. x) - ((f | X) /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A8, A13;



           A16: x0 in N2 by RCOMP_1: 16;

          (((f | X) /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A15, A16, A12, PARTFUN2: 15;

          then ((f /. x) - (f /. x0)) = ((L /. (x - x0)) + (R /. (x - x0))) by A14, A12, PARTFUN2: 15;

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

          hence thesis by A14, A11, PARTFUN2: 15;

        end;

        hence (f | Z) is_differentiable_in x0 by A11;

      end;

      hence thesis by A3;

    end;



     Lm1: ( {} REAL ) is closed;

    theorem :: NDIFF_3:25

    ex R be RestFunc of F st (R /. 0 ) = ( 0. F) & R is_continuous_in 0

    proof

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

      then

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

      set R = ( REAL --> ( 0. F));

      reconsider f = R as PartFunc of REAL , the carrier of F;



       A1: ( dom R) = REAL ;

      now

        let h;

        now

          let n be Nat;



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



           A3: n in NAT by ORDINAL1:def 12;



          thus (((h " ) (#) (R /* h)) . n) = (((h " ) . n) * ((R /* h) . n)) by NDIFF_1:def 2

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

          .= ( 0. F) by RLVECT_1: 10;

        end;

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

        hence ((h " ) (#) (R /* h)) is convergent & ( lim ((h " ) (#) (R /* h))) = ( 0. F) by NDIFF_1: 18;

      end;

      then

      reconsider R as RestFunc of F by Def1;

      set L = ( REAL --> ( 0. F));

      now

        let p be Real;

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



        thus (L /. p) = (L /. pp)

        .= ( 0. F)

        .= (p * ( 0. F)) by RLVECT_1: 10;

      end;

      then

      reconsider L as LinearFunc of F by Def2;



       A5: (f | Z) is constant;

      consider r be Point of F such that

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

       A7:

      now

        let x;

        assume

         A8: x in (Z /\ ( dom f));

        then x in ( dom f);



        hence (f /. x) = (f . x) by PARTFUN1:def 6

        .= r by A8, A6;

      end;

       A9:

      now

        let x0;

        assume

         A10: x0 in Z;

        set N = the Neighbourhood of x0;

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

        proof



           A12: x0 in (Z /\ ( dom f)) by A10;

          let x;



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



          then

           A14: (R /. (x - x0)) = (R . (x - x0)) by A1, PARTFUN1:def 6

          .= ( 0. F) by FUNCOP_1: 7, A13;

          assume x in N;

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



          hence ((f /. x) - (f /. x0)) = (r - (f /. x0)) by A7

          .= (r - r) by A7, A12

          .= ( 0. F) by RLVECT_1: 15

          .= (L . (x - x0)) by FUNCOP_1: 7, A13

          .= (L /. (x - x0)) by A1, PARTFUN1:def 6, A13

          .= ((L /. (x - x0)) + (R /. (x - x0))) by A14, RLVECT_1: 4;

        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

       A15: 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

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

      take R;

      consider p be Point of F such that

       A17: for r holds (L /. r) = (r * p) by Def2;

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

      then ( 0. F) = ((L /. (x0 - x0)) + (R /. (x0 - x0))) by RLVECT_1: 15;

      then ( 0. F) = (( 0 * p) + (R /. 0 )) by A17;

      then ( 0. F) = (( 0. F) + (R /. 0 )) by RLVECT_1: 10;

      hence

       A18: (R /. 0 ) = ( 0. F) by RLVECT_1: 4;

       A19:

      now

        set s3 = cs;

        let h;



         A20: (s3 . 1) = 0 ;

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

        then ||.((h " ) (#) (R /* h)).|| is bounded by LOPBAN_1: 20, SEQ_2: 13;

        then

        consider M be Real such that M > 0 and

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

         A22:

        now

          let n;

           |.( ||.((h " ) (#) (R /* h)).|| . n).| < M by A21;

          then |. ||.(((h " ) (#) (R /* h)) . n).||.| < M by NORMSP_0:def 4;

          hence ||.(((h " ) (#) (R /* h)) . n).|| < M by ABSVALUE:def 1;

        end;

        reconsider z0 = 0 as Real;

         A23:

        now

          let n be Element of NAT ;

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

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

          then

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

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

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

          then ||.((h . n) * (((h . n) " ) * ((R /* h) . n))).|| <= (M * |.(h . n).|) by NORMSP_1:def 1;

          then

           A25: ||.(((h . n) * ((h . n) " )) * ((R /* h) . n)).|| <= (M * |.(h . n).|) by RLVECT_1:def 7;

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

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

          then ||.((R /* h) . n).|| <= (M * |.(h . n).|) by RLVECT_1:def 8;

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

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

        end;

        ( lim h) = z0;



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

        .= z0 by ABSVALUE: 2;



        then

         A26: ( lim (M (#) ( abs h))) = (M * z0) by SEQ_2: 8

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

        reconsider z0 = 0 as Real;

        ( lim (M (#) ( abs h))) = 0 by A26, A20, SEQ_4: 25;

        hence (R /* h) is convergent & ( lim (R /* h)) = (R /. 0 ) by A18, A23, Th1;

      end;

      R is total by Def1;

      then

       A27: ( dom R) = REAL by FUNCT_2:def 1;

      now

        let s1;

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

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

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

        for n be Nat holds (s1 . n) <> 0 by A29;

        then s1 is non-zero by SEQ_1: 5;

        then s1 is 0 -convergent non-zero Real_Sequence by A28, FDIFF_1:def 1;

        hence (R /* s1) is convergent & (R /. ( In ( 0 , REAL ))) = ( lim (R /* s1)) by A19;

      end;

      hence thesis by A27, NFCONT_3: 7;

    end;

    definition

      let F;

      let f be PartFunc of REAL , the carrier of F;

      :: NDIFF_3:def7

      attr f is differentiable means

      : Def7: f is_differentiable_on ( dom f);

    end



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

    registration

      let F;

      cluster differentiable for Function of REAL , the carrier of F;

      existence

      proof

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

        reconsider f = ( REAL --> ( 0. F)) as Function of REAL , the carrier of F;

        take f;



         A1: Z = ( dom f);

        now

          let x;

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

          assume x in Z;



          thus (f /. x) = (f /. xx)

          .= ( 0. F)

          .= (x * ( 0. F)) by RLVECT_1: 10

          .= ((x * ( 0. F)) + ( 0. F)) by RLVECT_1: 4;

        end;

        then f is_differentiable_on Z by A1, Th21;

        hence thesis;

      end;

    end

    theorem :: NDIFF_3:26

    for f be differentiable PartFunc of REAL , the carrier of F st Z c= ( dom f) holds f is_differentiable_on Z by Def7, Th24;