fdiff_3.miz



    begin

    reserve h,h1,h2 for 0 -convergent non-zero Real_Sequence,

c,c1 for constant Real_Sequence,

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

x0,r,r0,r1,r2,g,g1,g2 for Real,

n0,k,n,m for Element of NAT ,

a,b,d for Real_Sequence,

x for set;

    theorem :: FDIFF_3:1

    

     Th1: (ex r st r > 0 & [.(x0 - r), x0.] c= ( dom f)) implies ex h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & for n be Nat holds (h . n) < 0

    proof

      given r such that

       A1: r > 0 and

       A2: [.(x0 - r), x0.] c= ( dom f);

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

      set a = ( seq_const x0);

      reconsider a as constant Real_Sequence;

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

      consider b such that

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

       A4:

      now

        let n be Nat;

         0 < (r / (n + 2)) by A1, XREAL_1: 139;

        then ( - (r / (n + 2))) < ( - 0 ) by XREAL_1: 24;

        then (( - r) / (n + 2)) < 0 by XCMPLX_1: 187;

        hence (b . n) < 0 by A3;

      end;

      then for n be Nat holds 0 <> (b . n);

      then

       A5: b is non-zero by SEQ_1: 5;

      b is convergent & ( lim b) = 0 by A3, SEQ_4: 31;

      then

      reconsider b as 0 -convergent non-zero Real_Sequence by A5, FDIFF_1:def 1;

      take b;

      take a;

      thus ( rng a) = {x0}

      proof

        thus ( rng a) c= {x0}

        proof

          let x be object;

          assume x in ( rng a);

          then ex n st x = (a . n) by FUNCT_2: 113;

          then x = x0 by SEQ_1: 57;

          hence thesis by TARSKI:def 1;

        end;

        let x be object;

        assume x in {x0};

        

        then x = x0 by TARSKI:def 1

        .= (a . 0 ) by SEQ_1: 57;

        hence thesis by VALUED_0: 28;

      end;

      thus ( rng (b + a)) c= ( dom f)

      proof

        let x be object;

        assume x in ( rng (b + a));

        then

        consider n such that

         A6: x = ((b + a) . n) by FUNCT_2: 113;

        ( 0 + 1) < (n + 2) by XREAL_1: 8;

        then (r * 1) < (r * (n + 2)) by A1, XREAL_1: 97;

        then (r * ((n + 2) " )) < ((r * (n + 2)) * ((n + 2) " )) by XREAL_1: 68;

        then (r * ((n + 2) " )) < (r * ((n + 2) * ((n + 2) " )));

        then (r * ((n + 2) " )) < (r * 1) by XCMPLX_0:def 7;

        then (r / (n + 2)) < r by XCMPLX_0:def 9;

        then (x0 - r) < (x0 - (r / (n + 2))) by XREAL_1: 15;

        then (x0 - r) < (x0 + ( - (r / (n + 2))));

        then

         A7: (x0 - r) <= (x0 + (( - r) / (n + 2))) by XCMPLX_1: 187;

         0 < (r / (n + 2)) by A1, XREAL_1: 139;

        then (x0 - (r / (n + 2))) < (x0 - 0 ) by XREAL_1: 15;

        then (x0 + ( - (r / (n + 2)))) <= x0;

        then (x0 + (( - r) / (n + 2))) <= x0 by XCMPLX_1: 187;

        then

         A8: (x0 + (( - r) / (n + 2))) in { g1 : (x0 - r) <= g1 & g1 <= x0 } by A7;

        x = ((b . n) + (a . n)) by A6, SEQ_1: 7

        .= ((( - r) / (n + 2)) + (a . n)) by A3

        .= (x0 + (( - r) / (n + 2))) by SEQ_1: 57;

        then x in [.(x0 - r), x0.] by A8, RCOMP_1:def 1;

        hence thesis by A2;

      end;

      thus thesis by A4;

    end;

    theorem :: FDIFF_3:2

    

     Th2: (ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f)) implies ex h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & for n be Nat holds (h . n) > 0

    proof

      given r such that

       A1: r > 0 and

       A2: [.x0, (x0 + r).] c= ( dom f);

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

      set a = ( seq_const x0);

      reconsider a as constant Real_Sequence;

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

      consider b such that

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

       A4:

      now

        let n be Nat;

         0 < (r / (n + 2)) by A1, XREAL_1: 139;

        hence 0 < (b . n) by A3;

      end;

      then for n be Nat holds 0 <> (b . n);

      then

       A5: b is non-zero by SEQ_1: 5;

      b is convergent & ( lim b) = 0 by A3, SEQ_4: 31;

      then

      reconsider b as 0 -convergent non-zero Real_Sequence by A5, FDIFF_1:def 1;

      take b, a;

      thus ( rng a) = {x0}

      proof

        thus ( rng a) c= {x0}

        proof

          let x be object;

          assume x in ( rng a);

          then ex n st x = (a . n) by FUNCT_2: 113;

          then x = x0 by SEQ_1: 57;

          hence thesis by TARSKI:def 1;

        end;

        let x be object;

        assume x in {x0};

        

        then x = x0 by TARSKI:def 1

        .= (a . 0 ) by SEQ_1: 57;

        hence thesis by VALUED_0: 28;

      end;

      thus ( rng (b + a)) c= ( dom f)

      proof

        let x be object;

        assume x in ( rng (b + a));

        then

        consider n such that

         A6: x = ((b + a) . n) by FUNCT_2: 113;

        ( 0 + 1) < (n + 2) by XREAL_1: 8;

        then (r * 1) < (r * (n + 2)) by A1, XREAL_1: 97;

        then (r * ((n + 2) " )) < ((r * (n + 2)) * ((n + 2) " )) by XREAL_1: 68;

        then (r * ((n + 2) " )) < (r * ((n + 2) * ((n + 2) " )));

        then (r * ((n + 2) " )) < (r * 1) by XCMPLX_0:def 7;

        then (r / (n + 2)) < r by XCMPLX_0:def 9;

        then

         A7: (x0 + (r / (n + 2))) <= (x0 + r) by XREAL_1: 6;

         0 < (r / (n + 2)) by A1, XREAL_1: 139;

        then (x0 + 0 ) < (x0 + (r / (n + 2))) by XREAL_1: 8;

        then

         A8: (x0 + (r / (n + 2))) in { g1 : x0 <= g1 & g1 <= (x0 + r) } by A7;

        x = ((b . n) + (a . n)) by A6, SEQ_1: 7

        .= ((r / (n + 2)) + (a . n)) by A3

        .= ((r / (n + 2)) + x0) by SEQ_1: 57;

        then x in [.x0, (x0 + r).] by A8, RCOMP_1:def 1;

        hence thesis by A2;

      end;

      thus thesis by A4;

    end;

    theorem :: FDIFF_3:3

    

     Th3: (for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent) & {x0} c= ( dom f) implies for h1, h2, c st ( rng c) = {x0} & ( rng (h1 + c)) c= ( dom f) & (for n be Nat holds (h1 . n) < 0 ) & ( rng (h2 + c)) c= ( dom f) & (for n be Nat holds (h2 . n) < 0 ) holds ( lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c)))) = ( lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))))

    proof

      assume that

       A1: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent and

       A2: {x0} c= ( dom f);

      let h1, h2, c such that

       A3: ( rng c) = {x0} and

       A4: ( rng (h1 + c)) c= ( dom f) and

       A5: for n be Nat holds (h1 . n) < 0 and

       A6: ( rng (h2 + c)) c= ( dom f) and

       A7: for n be Nat holds (h2 . n) < 0 ;

      deffunc G( Element of NAT ) = (h2 . $1);

      deffunc F( Element of NAT ) = (h1 . $1);

      consider d such that

       A8: for n holds (d . (2 * n)) = F(n) & (d . ((2 * n) + 1)) = G(n) from SCHEME1:sch 2;

      now

        let n be Nat;

        consider m such that

         A9: n = (2 * m) or n = ((2 * m) + 1) by SCHEME1: 1;

        now

          per cases by A9;

            suppose

             A10: n = (2 * m);

            (d . (2 * m)) = (h1 . m) by A8;

            hence (d . n) <> 0 by A10, SEQ_1: 5;

          end;

            suppose

             A11: n = ((2 * m) + 1);

            (d . ((2 * m) + 1)) = (h2 . m) by A8;

            hence (d . n) <> 0 by A11, SEQ_1: 5;

          end;

        end;

        hence (d . n) <> 0 ;

      end;

      then

       A12: d is non-zero by SEQ_1: 5;

      

       A13: h2 is convergent & ( lim h2) = 0 ;

      h1 is convergent & ( lim h1) = 0 ;

      then d is convergent & ( lim d) = 0 by A8, A13, FDIFF_2: 1;

      then

      reconsider d as 0 -convergent non-zero Real_Sequence by A12, FDIFF_1:def 1;

      deffunc F( Nat) = (2 * $1);

      consider a such that

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

      deffunc G( Nat) = ((2 * $1) + 1);

      consider b such that

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

      for n holds (b . n) = G(n) by A15;

      then

      reconsider b as increasing sequence of NAT by FDIFF_2: 3;

      

       A16: ( rng (d + c)) c= ( dom f)

      proof

        let x be object;

        assume x in ( rng (d + c));

        then

        consider n such that

         A17: x = ((d + c) . n) by FUNCT_2: 113;

        consider m such that

         A18: n = (2 * m) or n = ((2 * m) + 1) by SCHEME1: 1;

        

         A19: x = ((d . n) + (c . n)) by A17, SEQ_1: 7;

        now

          per cases by A18;

            suppose n = (2 * m);

            

            then x = ((h1 . m) + (c . (2 * m))) by A8, A19

            .= ((h1 . m) + (c . m)) by VALUED_0: 23

            .= ((h1 + c) . m) by SEQ_1: 7;

            then x in ( rng (h1 + c)) by VALUED_0: 28;

            hence thesis by A4;

          end;

            suppose n = ((2 * m) + 1);

            

            then x = ((h2 . m) + (c . ((2 * m) + 1))) by A8, A19

            .= ((h2 . m) + (c . m)) by VALUED_0: 23

            .= ((h2 + c) . m) by SEQ_1: 7;

            then x in ( rng (h2 + c)) by VALUED_0: 28;

            hence thesis by A6;

          end;

        end;

        hence thesis;

      end;

      now

        let n;

        

        thus ((((d " ) (#) ((f /* (d + c)) - (f /* c))) * b) . n) = (((d " ) (#) ((f /* (d + c)) - (f /* c))) . (b . n)) by FUNCT_2: 15

        .= (((d " ) (#) ((f /* (d + c)) - (f /* c))) . ((2 * n) + 1)) by A15

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

        .= (((d " ) . ((2 * n) + 1)) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1)))) by RFUNCT_2: 1

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

        .= (((h2 . n) " ) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1)))) by A8

        .= (((h2 " ) . n) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1)))) by VALUED_1: 10

        .= (((h2 " ) . n) * ((f . ((d + c) . ((2 * n) + 1))) - ((f /* c) . ((2 * n) + 1)))) by A16, FUNCT_2: 108

        .= (((h2 " ) . n) * ((f . ((d . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1)))) by SEQ_1: 7

        .= (((h2 " ) . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - ((f /* c) . ((2 * n) + 1)))) by A8

        .= (((h2 " ) . n) * ((f . ((h2 . n) + (c . n))) - ((f /* c) . ((2 * n) + 1)))) by VALUED_0: 23

        .= (((h2 " ) . n) * ((f . ((h2 + c) . n)) - ((f /* c) . ((2 * n) + 1)))) by SEQ_1: 7

        .= (((h2 " ) . n) * (((f /* (h2 + c)) . n) - ((f /* c) . ((2 * n) + 1)))) by A6, FUNCT_2: 108

        .= (((h2 " ) . n) * (((f /* (h2 + c)) . n) - (f . (c . ((2 * n) + 1))))) by A2, A3, FUNCT_2: 108

        .= (((h2 " ) . n) * (((f /* (h2 + c)) . n) - (f . (c . n)))) by VALUED_0: 23

        .= (((h2 " ) . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n))) by A2, A3, FUNCT_2: 108

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

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

      end;

      then

       A20: ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) is subsequence of ((d " ) (#) ((f /* (d + c)) - (f /* c))) by FUNCT_2: 63;

      now

        let n be Nat;

        consider m such that

         A21: n = (2 * m) or n = ((2 * m) + 1) by SCHEME1: 1;

        now

          per cases by A21;

            suppose

             A22: n = (2 * m);

            (d . (2 * m)) = (h1 . m) by A8;

            hence (d . n) < 0 by A5, A22;

          end;

            suppose

             A23: n = ((2 * m) + 1);

            (d . ((2 * m) + 1)) = (h2 . m) by A8;

            hence (d . n) < 0 by A7, A23;

          end;

        end;

        hence (d . n) < 0 ;

      end;

      then

       A24: ((d " ) (#) ((f /* (d + c)) - (f /* c))) is convergent by A1, A3, A16;

      for n holds (a . n) = F(n) by A14;

      then

      reconsider a as increasing sequence of NAT by FDIFF_2: 2;

      now

        let n;

        

        thus ((((d " ) (#) ((f /* (d + c)) - (f /* c))) * a) . n) = (((d " ) (#) ((f /* (d + c)) - (f /* c))) . (a . n)) by FUNCT_2: 15

        .= (((d " ) (#) ((f /* (d + c)) - (f /* c))) . (2 * n)) by A14

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

        .= (((d " ) . (2 * n)) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n)))) by RFUNCT_2: 1

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

        .= (((h1 . n) " ) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n)))) by A8

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

        .= (((h1 " ) . n) * ((f . ((d + c) . (2 * n))) - ((f /* c) . (2 * n)))) by A16, FUNCT_2: 108

        .= (((h1 " ) . n) * ((f . ((d . (2 * n)) + (c . (2 * n)))) - ((f /* c) . (2 * n)))) by SEQ_1: 7

        .= (((h1 " ) . n) * ((f . ((h1 . n) + (c . (2 * n)))) - ((f /* c) . (2 * n)))) by A8

        .= (((h1 " ) . n) * ((f . ((h1 . n) + (c . n))) - ((f /* c) . (2 * n)))) by VALUED_0: 23

        .= (((h1 " ) . n) * ((f . ((h1 + c) . n)) - ((f /* c) . (2 * n)))) by SEQ_1: 7

        .= (((h1 " ) . n) * (((f /* (h1 + c)) . n) - ((f /* c) . (2 * n)))) by A4, FUNCT_2: 108

        .= (((h1 " ) . n) * (((f /* (h1 + c)) . n) - (f . (c . (2 * n))))) by A2, A3, FUNCT_2: 108

        .= (((h1 " ) . n) * (((f /* (h1 + c)) . n) - (f . (c . n)))) by VALUED_0: 23

        .= (((h1 " ) . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n))) by A2, A3, FUNCT_2: 108

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

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

      end;

      then ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) is subsequence of ((d " ) (#) ((f /* (d + c)) - (f /* c))) by FUNCT_2: 63;

      then ( lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c)))) = ( lim ((d " ) (#) ((f /* (d + c)) - (f /* c)))) by A24, SEQ_4: 17;

      hence thesis by A24, A20, SEQ_4: 17;

    end;

    theorem :: FDIFF_3:4

    

     Th4: (for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent) & {x0} c= ( dom f) implies for h1, h2, c st ( rng c) = {x0} & ( rng (h1 + c)) c= ( dom f) & ( rng (h2 + c)) c= ( dom f) & (for n be Nat holds (h1 . n) > 0 ) & (for n be Nat holds (h2 . n) > 0 ) holds ( lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c)))) = ( lim ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))))

    proof

      assume that

       A1: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent and

       A2: {x0} c= ( dom f);

      let h1, h2, c such that

       A3: ( rng c) = {x0} and

       A4: ( rng (h1 + c)) c= ( dom f) and

       A5: ( rng (h2 + c)) c= ( dom f) and

       A6: for n be Nat holds (h1 . n) > 0 and

       A7: for n be Nat holds (h2 . n) > 0 ;

      deffunc G( Element of NAT ) = (h2 . $1);

      deffunc F( Element of NAT ) = (h1 . $1);

      consider d such that

       A8: for n holds (d . (2 * n)) = F(n) & (d . ((2 * n) + 1)) = G(n) from SCHEME1:sch 2;

      now

        let n be Nat;

        consider m such that

         A9: n = (2 * m) or n = ((2 * m) + 1) by SCHEME1: 1;

        now

          per cases by A9;

            suppose n = (2 * m);

            then (d . n) = (h1 . m) by A8;

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

          end;

            suppose n = ((2 * m) + 1);

            then (d . n) = (h2 . m) by A8;

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

          end;

        end;

        hence (d . n) <> 0 ;

      end;

      then

       A10: d is non-zero by SEQ_1: 5;

      

       A11: h2 is convergent & ( lim h2) = 0 ;

      h1 is convergent & ( lim h1) = 0 ;

      then d is convergent & ( lim d) = 0 by A8, A11, FDIFF_2: 1;

      then

      reconsider d as 0 -convergent non-zero Real_Sequence by A10, FDIFF_1:def 1;

      deffunc F( Nat) = (2 * $1);

      consider a such that

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

      deffunc G( Nat) = ((2 * $1) + 1);

      consider b such that

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

      for n holds (b . n) = G(n) by A13;

      then

      reconsider b as increasing sequence of NAT by FDIFF_2: 3;

      

       A14: ( rng (d + c)) c= ( dom f)

      proof

        let x be object;

        assume x in ( rng (d + c));

        then

        consider n such that

         A15: x = ((d + c) . n) by FUNCT_2: 113;

        consider m such that

         A16: n = (2 * m) or n = ((2 * m) + 1) by SCHEME1: 1;

        now

          per cases by A16;

            suppose n = (2 * m);

            

            then x = ((d . (2 * m)) + (c . (2 * m))) by A15, SEQ_1: 7

            .= ((h1 . m) + (c . (2 * m))) by A8

            .= ((h1 . m) + (c . m)) by VALUED_0: 23

            .= ((h1 + c) . m) by SEQ_1: 7;

            then x in ( rng (h1 + c)) by VALUED_0: 28;

            hence thesis by A4;

          end;

            suppose n = ((2 * m) + 1);

            

            then x = ((d . ((2 * m) + 1)) + (c . ((2 * m) + 1))) by A15, SEQ_1: 7

            .= ((h2 . m) + (c . ((2 * m) + 1))) by A8

            .= ((h2 . m) + (c . m)) by VALUED_0: 23

            .= ((h2 + c) . m) by SEQ_1: 7;

            then x in ( rng (h2 + c)) by VALUED_0: 28;

            hence thesis by A5;

          end;

        end;

        hence thesis;

      end;

      now

        let n;

        

        thus ((((d " ) (#) ((f /* (d + c)) - (f /* c))) * b) . n) = (((d " ) (#) ((f /* (d + c)) - (f /* c))) . (b . n)) by FUNCT_2: 15

        .= (((d " ) (#) ((f /* (d + c)) - (f /* c))) . ((2 * n) + 1)) by A13

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

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

        .= (((h2 . n) " ) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1))) by A8

        .= (((h2 " ) . n) * (((f /* (d + c)) - (f /* c)) . ((2 * n) + 1))) by VALUED_1: 10

        .= (((h2 " ) . n) * (((f /* (d + c)) . ((2 * n) + 1)) - ((f /* c) . ((2 * n) + 1)))) by RFUNCT_2: 1

        .= (((h2 " ) . n) * ((f . ((d + c) . ((2 * n) + 1))) - ((f /* c) . ((2 * n) + 1)))) by A14, FUNCT_2: 108

        .= (((h2 " ) . n) * ((f . ((d + c) . ((2 * n) + 1))) - (f . (c . ((2 * n) + 1))))) by A2, A3, FUNCT_2: 108

        .= (((h2 " ) . n) * ((f . ((d . ((2 * n) + 1)) + (c . ((2 * n) + 1)))) - (f . (c . ((2 * n) + 1))))) by SEQ_1: 7

        .= (((h2 " ) . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - (f . (c . ((2 * n) + 1))))) by A8

        .= (((h2 " ) . n) * ((f . ((h2 . n) + (c . ((2 * n) + 1)))) - (f . (c . n)))) by VALUED_0: 23

        .= (((h2 " ) . n) * ((f . ((h2 . n) + (c . n))) - (f . (c . n)))) by VALUED_0: 23

        .= (((h2 " ) . n) * ((f . ((h2 + c) . n)) - (f . (c . n)))) by SEQ_1: 7

        .= (((h2 " ) . n) * (((f /* (h2 + c)) . n) - (f . (c . n)))) by A5, FUNCT_2: 108

        .= (((h2 " ) . n) * (((f /* (h2 + c)) . n) - ((f /* c) . n))) by A2, A3, FUNCT_2: 108

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

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

      end;

      then

       A17: ((h2 " ) (#) ((f /* (h2 + c)) - (f /* c))) is subsequence of ((d " ) (#) ((f /* (d + c)) - (f /* c))) by FUNCT_2: 63;

      for n be Nat holds (d . n) > 0

      proof

        let n be Nat;

        consider m such that

         A18: n = (2 * m) or n = ((2 * m) + 1) by SCHEME1: 1;

        now

          per cases by A18;

            suppose n = (2 * m);

            then (d . n) = (h1 . m) by A8;

            hence thesis by A6;

          end;

            suppose n = ((2 * m) + 1);

            then (d . n) = (h2 . m) by A8;

            hence thesis by A7;

          end;

        end;

        hence thesis;

      end;

      then

       A19: ((d " ) (#) ((f /* (d + c)) - (f /* c))) is convergent by A1, A3, A14;

      for n holds (a . n) = F(n) by A12;

      then

      reconsider a as increasing sequence of NAT by FDIFF_2: 2;

      now

        let n;

        

        thus ((((d " ) (#) ((f /* (d + c)) - (f /* c))) * a) . n) = (((d " ) (#) ((f /* (d + c)) - (f /* c))) . (a . n)) by FUNCT_2: 15

        .= (((d " ) (#) ((f /* (d + c)) - (f /* c))) . (2 * n)) by A12

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

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

        .= (((h1 . n) " ) * (((f /* (d + c)) - (f /* c)) . (2 * n))) by A8

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

        .= (((h1 " ) . n) * (((f /* (d + c)) . (2 * n)) - ((f /* c) . (2 * n)))) by RFUNCT_2: 1

        .= (((h1 " ) . n) * ((f . ((d + c) . (2 * n))) - ((f /* c) . (2 * n)))) by A14, FUNCT_2: 108

        .= (((h1 " ) . n) * ((f . ((d + c) . (2 * n))) - (f . (c . (2 * n))))) by A2, A3, FUNCT_2: 108

        .= (((h1 " ) . n) * ((f . ((d . (2 * n)) + (c . (2 * n)))) - (f . (c . (2 * n))))) by SEQ_1: 7

        .= (((h1 " ) . n) * ((f . ((h1 . n) + (c . (2 * n)))) - (f . (c . (2 * n))))) by A8

        .= (((h1 " ) . n) * ((f . ((h1 . n) + (c . (2 * n)))) - (f . (c . n)))) by VALUED_0: 23

        .= (((h1 " ) . n) * ((f . ((h1 . n) + (c . n))) - (f . (c . n)))) by VALUED_0: 23

        .= (((h1 " ) . n) * ((f . ((h1 + c) . n)) - (f . (c . n)))) by SEQ_1: 7

        .= (((h1 " ) . n) * (((f /* (h1 + c)) . n) - (f . (c . n)))) by A4, FUNCT_2: 108

        .= (((h1 " ) . n) * (((f /* (h1 + c)) . n) - ((f /* c) . n))) by A2, A3, FUNCT_2: 108

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

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

      end;

      then ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c))) is subsequence of ((d " ) (#) ((f /* (d + c)) - (f /* c))) by FUNCT_2: 63;

      then ( lim ((h1 " ) (#) ((f /* (h1 + c)) - (f /* c)))) = ( lim ((d " ) (#) ((f /* (d + c)) - (f /* c)))) by A19, SEQ_4: 17;

      hence thesis by A19, A17, SEQ_4: 17;

    end;

    definition

      let f, x0;

      :: FDIFF_3:def1

      pred f is_Lcontinuous_in x0 means x0 in ( dom f) & for a st ( rng a) c= (( left_open_halfline x0) /\ ( dom f)) & a is convergent & ( lim a) = x0 holds (f /* a) is convergent & (f . x0) = ( lim (f /* a));

      :: FDIFF_3:def2

      pred f is_Rcontinuous_in x0 means x0 in ( dom f) & for a st ( rng a) c= (( right_open_halfline x0) /\ ( dom f)) & a is convergent & ( lim a) = x0 holds (f /* a) is convergent & (f . x0) = ( lim (f /* a));

      :: FDIFF_3:def3

      pred f is_right_differentiable_in x0 means (ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f)) & for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent;

      :: FDIFF_3:def4

      pred f is_left_differentiable_in x0 means (ex r st r > 0 & [.(x0 - r), x0.] c= ( dom f)) & for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent;

    end

    theorem :: FDIFF_3:5

    

     Th5: f is_left_differentiable_in x0 implies f is_Lcontinuous_in x0

    proof

      assume

       A1: f is_left_differentiable_in x0;

      

       A2: for a st ( rng a) c= (( left_open_halfline x0) /\ ( dom f)) & a is convergent & ( lim a) = x0 holds (f /* a) is convergent & (f . x0) = ( lim (f /* a))

      proof

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

        set b = ( seq_const x0);

        let a such that

         A3: ( rng a) c= (( left_open_halfline x0) /\ ( dom f)) and

         A4: a is convergent and

         A5: ( lim a) = x0;

        consider r such that

         A6: 0 < r and

         A7: [.(x0 - r), x0.] c= ( dom f) by A1;

        consider n0 be Nat such that

         A8: for k be Nat st k >= n0 holds (x0 - r) < (a . k) by A4, A5, A6, LIMFUNC2: 1, XREAL_1: 44;

        deffunc F( Nat) = ((a . $1) - (b . $1));

        consider d such that

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

        

         A10: d = (a - b) by A9, RFUNCT_2: 1;

        then

         A11: d is convergent by A4;

        reconsider c = (b ^\ n0) as constant Real_Sequence;

        

         A12: ( rng c) = {x0}

        proof

          thus ( rng c) c= {x0}

          proof

            let x be object;

            assume x in ( rng c);

            then

            consider n such that

             A13: x = ((b ^\ n0) . n) by FUNCT_2: 113;

            x = (b . (n + n0)) by A13, NAT_1:def 3;

            then x = x0 by SEQ_1: 57;

            hence thesis by TARSKI:def 1;

          end;

          let x be object;

          assume x in {x0};

          then

           A14: x = x0 by TARSKI:def 1;

          (c . 0 ) = (b . ( 0 + n0)) by NAT_1:def 3

          .= x by A14, SEQ_1: 57;

          hence thesis by VALUED_0: 28;

        end;

         A15:

        now

          let g be Real such that

           A16: 0 < g;

          reconsider n = 0 as Nat;

          take n;

          let m be Nat such that n <= m;

          

           A17: m in NAT by ORDINAL1:def 12;

          (x0 - r) <= x0 by A6, XREAL_1: 44;

          then x0 in [.(x0 - r), x0.] by XXREAL_1: 1;

          then ( rng c) c= ( dom f) by A7, A12, ZFMISC_1: 31;

          

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

          .= |.((f . (b . (m + n0))) - (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)).| < g by A16;

        end;

        then

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

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

        .= x0 by SEQ_1: 57;

        

        then ( lim d) = (x0 - x0) by A4, A5, A10, SEQ_2: 12

        .= 0 ;

        then

         A19: ( lim (d ^\ n0)) = 0 by A11, SEQ_4: 20;

        

         A20: for n holds (d . n) < 0 & (d . n) <> 0

        proof

          let n;

          

           A21: (d . n) = ((a . n) - (b . n)) by A9;

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

          then (a . n) in ( left_open_halfline x0) by A3, XBOOLE_0:def 4;

          then (a . n) in { r1 : r1 < x0 } by XXREAL_1: 229;

          then

           A22: ex r1 st r1 = (a . n) & r1 < x0;

          then ((a . n) - x0) < (x0 - x0) by XREAL_1: 9;

          hence (d . n) < 0 by A21, SEQ_1: 57;

          thus thesis by A21, A22, SEQ_1: 57;

        end;

        

         A23: for n be Nat holds ((d ^\ n0) . n) < 0

        proof

          let n be Nat;

          

           A24: (n + n0) in NAT by ORDINAL1:def 12;

          ((d ^\ n0) . n) = (d . (n + n0)) by NAT_1:def 3;

          hence thesis by A20, A24;

        end;

        for n be Nat holds ((d ^\ n0) . n) <> 0 by A23;

        then (d ^\ n0) is non-zero by SEQ_1: 5;

        then

        reconsider h = (d ^\ n0) as 0 -convergent non-zero Real_Sequence by A11, A19, FDIFF_1:def 1;

        

         A25: ( rng a) c= ( dom f) by A3, XBOOLE_0:def 4;

        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) = ((((a - b) + b) ^\ n0) . n) by A10, SEQM_3: 15

          .= (((a - b) + b) . (n + n0)) by NAT_1:def 3

          .= (((a - b) . (n + n0)) + (b . (n + n0))) by SEQ_1: 7

          .= (((a . (n + n0)) - (b . (n + n0))) + (b . (n + n0))) by RFUNCT_2: 1

          .= ((a ^\ n0) . n) by NAT_1:def 3;

        end;

        

        then

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

        .= ((f /* a) ^\ n0) by A25, VALUED_0: 27;

        

         A28: for n holds ((a ^\ n0) . n) in [.(x0 - r), x0.]

        proof

          let n;

          (a . (n + n0)) in ( rng a) by VALUED_0: 28;

          then ((a ^\ n0) . n) in ( rng a) by NAT_1:def 3;

          then ((a ^\ n0) . n) in ( left_open_halfline x0) by A3, XBOOLE_0:def 4;

          then ((a ^\ n0) . n) in { g : g < x0 } by XXREAL_1: 229;

          then

           A29: ex g st g = ((a ^\ n0) . n) & g < x0;

           0 <= n & ( 0 + n0) = n0;

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

          then (x0 - r) <= (a . (n + n0)) by A8;

          then (x0 - r) <= ((a ^\ n0) . n) by NAT_1:def 3;

          then ((a ^\ n0) . n) in { g : (x0 - r) <= g & g <= x0 } by A29;

          hence thesis by RCOMP_1:def 1;

        end;

        ( rng (h + c)) c= [.(x0 - r), x0.]

        proof

          let x be object;

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

          then

          consider n such that

           A30: x = ((h + c) . n) by FUNCT_2: 113;

          ((h + c) . n) = ((((a - b) + b) ^\ n0) . n) by A10, SEQM_3: 15

          .= (((a - b) + b) . (n + n0)) by NAT_1:def 3

          .= (((a - b) . (n + n0)) + (b . (n + n0))) by SEQ_1: 7

          .= (((a . (n + n0)) - (b . (n + n0))) + (b . (n + n0))) by RFUNCT_2: 1

          .= ((a ^\ n0) . n) by NAT_1:def 3;

          hence thesis by A28, A30;

        end;

        then ( rng (h + c)) c= ( dom f) by A7;

        then

         A31: ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A1, A23, A12;

        

        then

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

        .= 0 ;

        now

          let n;

          

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

          

          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 A33, XCMPLX_0:def 7

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

        end;

        then

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

        then

         A35: ((f /* (h + c)) - (f /* c)) is convergent by A31;

        then

         A36: (((f /* (h + c)) - (f /* c)) + (f /* c)) is convergent by A18;

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

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

        

        then ( lim (((f /* (h + c)) - (f /* c)) + (f /* c))) = ( 0 + (f . x0)) by A32, A34, A35, A18, SEQ_2: 6

        .= (f . x0);

        hence thesis by A36, A27, SEQ_4: 22;

      end;

      x0 in ( dom f)

      proof

        consider r such that

         A37: 0 < r and

         A38: [.(x0 - r), x0.] c= ( dom f) by A1;

        (x0 - r) <= x0 by A37, XREAL_1: 44;

        then x0 in [.(x0 - r), x0.] by XXREAL_1: 1;

        hence thesis by A38;

      end;

      hence thesis by A2;

    end;

    theorem :: FDIFF_3:6

    

     Th6: f is_Lcontinuous_in x0 & (f . x0) <> g2 & (ex r st r > 0 & [.(x0 - r), x0.] c= ( dom f)) implies ex r1 st r1 > 0 & [.(x0 - r1), x0.] c= ( dom f) & for g st g in [.(x0 - r1), x0.] holds (f . g) <> g2

    proof

      assume that

       A1: f is_Lcontinuous_in x0 and

       A2: (f . x0) <> g2;

      given r such that

       A3: r > 0 and

       A4: [.(x0 - r), x0.] c= ( dom f);

      defpred P[ Element of NAT , set] means $2 in [.(x0 - (r / ($1 + 1))), x0.] & $2 in ( dom f) & (f . $2) = g2;

      assume

       A5: for r1 st r1 > 0 & [.(x0 - r1), x0.] c= ( dom f) holds ex g st g in [.(x0 - r1), x0.] & (f . g) = g2;

      

       A6: for n holds ex g be Element of REAL st P[n, g]

      proof

        let n;

        (x0 - r) <= x0 by A3, XREAL_1: 44;

        then

         A7: x0 in [.(x0 - r), x0.] by XXREAL_1: 1;

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

        then (r / (n + 1)) <= (r / 1) by A3, XREAL_1: 118;

        then

         A8: (x0 - r) <= (x0 - (r / (n + 1))) by XREAL_1: 13;

        (x0 - (r / (n + 1))) <= x0 by A3, XREAL_1: 44, XREAL_1: 139;

        then (x0 - (r / (n + 1))) in { g1 : (x0 - r) <= g1 & g1 <= x0 } by A8;

        then (x0 - (r / (n + 1))) in [.(x0 - r), x0.] by RCOMP_1:def 1;

        then [.(x0 - (r / (n + 1))), x0.] c= [.(x0 - r), x0.] by A7, XXREAL_2:def 12;

        then

         A9: [.(x0 - (r / (n + 1))), x0.] c= ( dom f) by A4;

        then

        consider g such that

         A10: g in [.(x0 - (r / (n + 1))), x0.] & (f . g) = g2 by A3, A5, XREAL_1: 139;

        take g;

        thus thesis by A9, A10;

      end;

      consider a such that

       A11: for n holds P[n, (a . n)] from FUNCT_2:sch 3( A6);

      

       A12: ( rng a) c= (( left_open_halfline x0) /\ ( dom f))

      proof

        let x be object;

        assume x in ( rng a);

        then

        consider n such that

         A13: x = (a . n) by FUNCT_2: 113;

        (a . n) in [.(x0 - (r / (n + 1))), x0.] by A11;

        then (a . n) in { g1 : (x0 - (r / (n + 1))) <= g1 & g1 <= x0 } by RCOMP_1:def 1;

        then

         A14: ex g1 st g1 = (a . n) & (x0 - (r / (n + 1))) <= g1 & g1 <= x0;

        (a . n) <> x0 by A2, A11;

        then (a . n) < x0 by A14, XXREAL_0: 1;

        then (a . n) in { g1 : g1 < x0 };

        then

         A15: (a . n) in ( left_open_halfline x0) by XXREAL_1: 229;

        (a . n) in ( dom f) by A11;

        hence thesis by A13, A15, XBOOLE_0:def 4;

      end;

      

       A16: (( left_open_halfline x0) /\ ( dom f)) c= ( dom f) by XBOOLE_1: 17;

      

       A17: for n holds ((f /* a) . n) = g2

      proof

        let n;

        

        thus ((f /* a) . n) = (f . (a . n)) by A12, A16, FUNCT_2: 108, XBOOLE_1: 1

        .= g2 by A11;

      end;

      now

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then ((f /* a) . n) = g2 by A17;

        hence ((f /* a) . n) = ((f /* a) . (n + 1)) by A17;

      end;

      

      then

       A18: ( lim (f /* a)) = ((f /* a) . 0 ) by SEQ_4: 26, VALUED_0: 25

      .= g2 by A17;

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

      set d = ( seq_const x0);

      deffunc F( Nat) = (x0 - (r / ($1 + 1)));

      consider b such that

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

       A20:

      now

        let n be Nat;

        

         A21: n in NAT by ORDINAL1:def 12;

        (a . n) in [.(x0 - (r / (n + 1))), x0.] by A11, A21;

        then (a . n) in { g1 : (x0 - (r / (n + 1))) <= g1 & g1 <= x0 } by RCOMP_1:def 1;

        then ex g1 st g1 = (a . n) & (x0 - (r / (n + 1))) <= g1 & g1 <= x0;

        hence (b . n) <= (a . n) & (a . n) <= (d . n) by A19, SEQ_1: 57;

      end;

      

       A22: ( lim d) = (d . 0 ) by SEQ_4: 26

      .= x0 by SEQ_1: 57;

      b is convergent & ( lim b) = x0 by A19, FCONT_3: 5;

      then a is convergent & ( lim a) = x0 by A22, A20, SEQ_2: 19, SEQ_2: 20;

      hence contradiction by A1, A2, A12, A18;

    end;

    theorem :: FDIFF_3:7

    

     Th7: f is_right_differentiable_in x0 implies f is_Rcontinuous_in x0

    proof

      assume

       A1: f is_right_differentiable_in x0;

      then

      consider r such that

       A2: r > 0 and

       A3: [.x0, (x0 + r).] c= ( dom f);

      

       A4: for a st ( rng a) c= (( right_open_halfline x0) /\ ( dom f)) & a is convergent & ( lim a) = x0 holds (f /* a) is convergent & (f . x0) = ( lim (f /* a))

      proof

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

        set b = ( seq_const x0);

        let a such that

         A5: ( rng a) c= (( right_open_halfline x0) /\ ( dom f)) and

         A6: a is convergent and

         A7: ( lim a) = x0;

        consider r such that

         A8: r > 0 and

         A9: [.x0, (x0 + r).] c= ( dom f) by A1;

        (x0 + 0 ) < (x0 + r) by A8, XREAL_1: 6;

        then

        consider n0 be Nat such that

         A10: for k be Nat st k >= n0 holds (a . k) < (x0 + r) by A6, A7, LIMFUNC2: 2;

        deffunc F( Nat) = ((a . $1) - (b . $1));

        consider d such that

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

        

         A12: d = (a - b) by A11, RFUNCT_2: 1;

        then

         A13: d is convergent by A6;

        reconsider c = (b ^\ n0) as constant Real_Sequence;

        

         A14: ( rng c) = {x0}

        proof

          thus ( rng c) c= {x0}

          proof

            let x be object;

            assume x in ( rng c);

            then

            consider n such that

             A15: x = ((b ^\ n0) . n) by FUNCT_2: 113;

            x = (b . (n + n0)) by A15, NAT_1:def 3;

            then x = x0 by SEQ_1: 57;

            hence thesis by TARSKI:def 1;

          end;

          let x be object;

          assume x in {x0};

          then

           A16: x = x0 by TARSKI:def 1;

          (c . 0 ) = (b . ( 0 + n0)) by NAT_1:def 3

          .= x by A16, SEQ_1: 57;

          hence thesis by VALUED_0: 28;

        end;

         A17:

        now

          let g be Real such that

           A18: 0 < g;

          reconsider n = 0 as Nat;

          take n;

          let m be Nat such that n <= m;

          

           A19: m in NAT by ORDINAL1:def 12;

          (x0 + 0 ) <= (x0 + r) by A8, XREAL_1: 7;

          then x0 in [.x0, (x0 + r).] by XXREAL_1: 1;

          then ( rng c) c= ( dom f) by A9, A14, ZFMISC_1: 31;

          

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

          .= |.((f . (b . (m + n0))) - (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)).| < g by A18;

        end;

        then

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

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

        .= x0 by SEQ_1: 57;

        

        then ( lim d) = (x0 - x0) by A6, A7, A12, SEQ_2: 12

        .= 0 ;

        then

         A21: ( lim (d ^\ n0)) = 0 by A13, SEQ_4: 20;

        

         A22: for n holds (d . n) > 0 & (d . n) <> 0

        proof

          let n;

          

           A23: (d . n) = ((a . n) - (b . n)) by A11;

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

          then (a . n) in ( right_open_halfline x0) by A5, XBOOLE_0:def 4;

          then (a . n) in { r1 : x0 < r1 } by XXREAL_1: 230;

          then

           A24: ex r1 st r1 = (a . n) & x0 < r1;

          then ((a . n) - x0) > (x0 - x0) by XREAL_1: 9;

          hence (d . n) > 0 by A23, SEQ_1: 57;

          thus thesis by A23, A24, SEQ_1: 57;

        end;

        

         A25: for n be Nat holds ((d ^\ n0) . n) > 0

        proof

          let n be Nat;

          

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

          ((d ^\ n0) . n) = (d . (n + n0)) by NAT_1:def 3;

          hence thesis by A22, A26;

        end;

        for n be Nat holds ((d ^\ n0) . n) <> 0 by A25;

        then (d ^\ n0) is non-zero by SEQ_1: 5;

        then

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

        

         A27: ( rng a) c= ( dom f) by A5, XBOOLE_0:def 4;

        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

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

        now

          let n;

          

          thus ((h + c) . n) = ((((a - b) + b) ^\ n0) . n) by A12, SEQM_3: 15

          .= (((a - b) + b) . (n + n0)) by NAT_1:def 3

          .= (((a - b) . (n + n0)) + (b . (n + n0))) by SEQ_1: 7

          .= (((a . (n + n0)) - (b . (n + n0))) + (b . (n + n0))) by RFUNCT_2: 1

          .= ((a ^\ n0) . n) by NAT_1:def 3;

        end;

        

        then

         A29: (((f /* (h + c)) - (f /* c)) + (f /* c)) = (f /* (a ^\ n0)) by A28, FUNCT_2: 63

        .= ((f /* a) ^\ n0) by A27, VALUED_0: 27;

        

         A30: for n holds ((a ^\ n0) . n) in [.x0, (x0 + r).]

        proof

          let n;

          (a . (n + n0)) in ( rng a) by VALUED_0: 28;

          then ((a ^\ n0) . n) in ( rng a) by NAT_1:def 3;

          then ((a ^\ n0) . n) in ( right_open_halfline x0) by A5, XBOOLE_0:def 4;

          then ((a ^\ n0) . n) in { g : x0 < g } by XXREAL_1: 230;

          then

           A31: ex g st g = ((a ^\ n0) . n) & x0 < g;

           0 <= n & ( 0 + n0) = n0;

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

          then (a . (n + n0)) <= (x0 + r) by A10;

          then ((a ^\ n0) . n) <= (x0 + r) by NAT_1:def 3;

          then ((a ^\ n0) . n) in { g : x0 <= g & g <= (x0 + r) } by A31;

          hence thesis by RCOMP_1:def 1;

        end;

        ( rng (h + c)) c= [.x0, (x0 + r).]

        proof

          let x be object;

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

          then

          consider n such that

           A32: x = ((h + c) . n) by FUNCT_2: 113;

          ((h + c) . n) = ((((a - b) + b) ^\ n0) . n) by A12, SEQM_3: 15

          .= (((a - b) + b) . (n + n0)) by NAT_1:def 3

          .= (((a - b) . (n + n0)) + (b . (n + n0))) by SEQ_1: 7

          .= (((a . (n + n0)) - (b . (n + n0))) + (b . (n + n0))) by RFUNCT_2: 1

          .= ((a ^\ n0) . n) by NAT_1:def 3;

          hence thesis by A30, A32;

        end;

        then ( rng (h + c)) c= ( dom f) by A9;

        then

         A33: ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A1, A25, A14;

        

        then

         A34: ( 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;

          

           A35: (h . n) <> 0 by A25;

          

          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 A35, XCMPLX_0:def 7

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

        end;

        then

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

        then

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

        then

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

        hence (f /* a) is convergent by A29, 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 A34, A36, A37, A20, SEQ_2: 6

        .= (f . x0);

        hence thesis by A38, A29, SEQ_4: 22;

      end;

      (x0 + 0 ) <= (x0 + r) by A2, XREAL_1: 7;

      then x0 in [.x0, (x0 + r).] by XXREAL_1: 1;

      hence thesis by A3, A4;

    end;

    theorem :: FDIFF_3:8

    

     Th8: f is_Rcontinuous_in x0 & (f . x0) <> g2 & (ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f)) implies ex r1 st r1 > 0 & [.x0, (x0 + r1).] c= ( dom f) & for g st g in [.x0, (x0 + r1).] holds (f . g) <> g2

    proof

      assume that

       A1: f is_Rcontinuous_in x0 and

       A2: (f . x0) <> g2;

      given r such that

       A3: r > 0 and

       A4: [.x0, (x0 + r).] c= ( dom f);

      defpred P[ Element of NAT , set] means $2 in [.x0, (x0 + (r / ($1 + 1))).] & $2 in ( dom f) & (f . $2) = g2;

      assume

       A5: for r1 st r1 > 0 & [.x0, (x0 + r1).] c= ( dom f) holds ex g st g in [.x0, (x0 + r1).] & (f . g) = g2;

      

       A6: for n holds ex g be Element of REAL st P[n, g]

      proof

        let n;

        (x0 + 0 ) <= (x0 + r) by A3, XREAL_1: 7;

        then

         A7: x0 in [.x0, (x0 + r).] by XXREAL_1: 1;

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

        then (r / (n + 1)) <= (r / 1) by A3, XREAL_1: 118;

        then

         A8: (x0 + (r / (n + 1))) <= (x0 + r) by XREAL_1: 7;

        (x0 + 0 ) = x0;

        then x0 <= (x0 + (r / (n + 1))) by A3, XREAL_1: 7;

        then (x0 + (r / (n + 1))) in { g1 : x0 <= g1 & g1 <= (x0 + r) } by A8;

        then (x0 + (r / (n + 1))) in [.x0, (x0 + r).] by RCOMP_1:def 1;

        then [.x0, (x0 + (r / (n + 1))).] c= [.x0, (x0 + r).] by A7, XXREAL_2:def 12;

        then

         A9: [.x0, (x0 + (r / (n + 1))).] c= ( dom f) by A4;

        then

        consider g such that

         A10: g in [.x0, (x0 + (r / (n + 1))).] & (f . g) = g2 by A3, A5, XREAL_1: 139;

        take g;

        thus thesis by A9, A10;

      end;

      consider a such that

       A11: for n holds P[n, (a . n)] from FUNCT_2:sch 3( A6);

      

       A12: ( rng a) c= (( right_open_halfline x0) /\ ( dom f))

      proof

        let x be object;

        assume x in ( rng a);

        then

        consider n such that

         A13: x = (a . n) by FUNCT_2: 113;

        (a . n) in [.x0, (x0 + (r / (n + 1))).] by A11;

        then (a . n) in { g1 : x0 <= g1 & g1 <= (x0 + (r / (n + 1))) } by RCOMP_1:def 1;

        then

         A14: ex g1 st g1 = (a . n) & x0 <= g1 & g1 <= (x0 + (r / (n + 1)));

        x0 <> (a . n) by A2, A11;

        then x0 < (a . n) by A14, XXREAL_0: 1;

        then (a . n) in { g1 : x0 < g1 };

        then

         A15: (a . n) in ( right_open_halfline x0) by XXREAL_1: 230;

        (a . n) in ( dom f) by A11;

        hence thesis by A13, A15, XBOOLE_0:def 4;

      end;

      

       A16: (( right_open_halfline x0) /\ ( dom f)) c= ( dom f) by XBOOLE_1: 17;

      

       A17: for n holds ((f /* a) . n) = g2

      proof

        let n;

        

        thus g2 = (f . (a . n)) by A11

        .= ((f /* a) . n) by A12, A16, FUNCT_2: 108, XBOOLE_1: 1;

      end;

      now

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then ((f /* a) . n) = g2 by A17;

        hence ((f /* a) . n) = ((f /* a) . (n + 1)) by A17;

      end;

      

      then

       A18: ( lim (f /* a)) = ((f /* a) . 0 ) by SEQ_4: 26, VALUED_0: 25

      .= g2 by A17;

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

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

      set b = ( seq_const x0);

      

       A19: ( lim b) = (b . 0 ) by SEQ_4: 26

      .= x0 by SEQ_1: 57;

      consider d such that

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

       A21:

      now

        let n be Nat;

        

         A22: n in NAT by ORDINAL1:def 12;

        (a . n) in [.x0, (x0 + (r / (n + 1))).] by A11, A22;

        then (a . n) in { g1 : x0 <= g1 & g1 <= (x0 + (r / (n + 1))) } by RCOMP_1:def 1;

        then ex g1 st g1 = (a . n) & x0 <= g1 & g1 <= (x0 + (r / (n + 1)));

        hence (b . n) <= (a . n) & (a . n) <= (d . n) by A20, SEQ_1: 57;

      end;

      d is convergent & ( lim d) = x0 by A20, FCONT_3: 6;

      then a is convergent & ( lim a) = x0 by A19, A21, SEQ_2: 19, SEQ_2: 20;

      hence contradiction by A1, A2, A12, A18;

    end;

    definition

      let x0, f;

      assume

       A1: f is_left_differentiable_in x0;

      :: FDIFF_3:def5

      func Ldiff (f,x0) -> Real means

      : Def5: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds it = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))));

      existence

      proof

        

         A2: {x0} c= ( dom f)

        proof

          let x be object;

          assume x in {x0};

          then

           A3: x = x0 by TARSKI:def 1;

          consider r such that

           A4: r > 0 and

           A5: [.(x0 - r), x0.] c= ( dom f) by A1;

          (x0 - r) <= x0 by A4, XREAL_1: 44;

          then x0 in [.(x0 - r), x0.] by XXREAL_1: 1;

          hence thesis by A3, A5;

        end;

        

         A6: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A1;

        ex r st r > 0 & [.(x0 - r), x0.] c= ( dom f) by A1;

        then

        consider h1, c1 such that

         A7: ( rng c1) = {x0} and

         A8: ( rng (h1 + c1)) c= ( dom f) & for n be Nat holds (h1 . n) < 0 by Th1;

        take ( lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))));

        let h, c such that

         A9: ( rng c) = {x0} and

         A10: ( rng (h + c)) c= ( dom f) & for n be Nat holds (h . n) < 0 ;

        c1 = c by A7, A9, FDIFF_2: 5;

        hence thesis by A7, A8, A2, A10, A6, Th3;

      end;

      uniqueness

      proof

        ex r st r > 0 & [.(x0 - r), x0.] c= ( dom f) by A1;

        then

        consider h, c such that

         A11: ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & for n be Nat holds (h . n) < 0 by Th1;

        let g1,g2 be Real such that

         A12: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds g1 = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) and

         A13: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds g2 = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))));

        g1 = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) by A12, A11;

        hence thesis by A13, A11;

      end;

    end

    definition

      let x0, f;

      assume

       A1: f is_right_differentiable_in x0;

      :: FDIFF_3:def6

      func Rdiff (f,x0) -> Real means

      : Def6: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds it = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))));

      existence

      proof

        

         A2: {x0} c= ( dom f)

        proof

          let x be object;

          assume x in {x0};

          then

           A3: x = x0 by TARSKI:def 1;

          consider r such that

           A4: r > 0 and

           A5: [.x0, (x0 + r).] c= ( dom f) by A1;

          (x0 + 0 ) <= (x0 + r) by A4, XREAL_1: 7;

          then x0 in [.x0, (x0 + r).] by XXREAL_1: 1;

          hence thesis by A3, A5;

        end;

        

         A6: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A1;

        ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f) by A1;

        then

        consider h, c such that

         A7: ( rng c) = {x0} and

         A8: ( rng (h + c)) c= ( dom f) & for n be Nat holds (h . n) > 0 by Th2;

        take ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))));

        let h1, c1 such that

         A9: ( rng c1) = {x0} and

         A10: ( rng (h1 + c1)) c= ( dom f) & for n be Nat holds (h1 . n) > 0 ;

        c1 = c by A7, A9, FDIFF_2: 5;

        hence thesis by A7, A8, A10, A6, A2, Th4;

      end;

      uniqueness

      proof

        ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f) by A1;

        then

        consider h, c such that

         A11: ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & for n be Nat holds (h . n) > 0 by Th2;

        let g1,g2 be Real such that

         A12: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds g1 = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) and

         A13: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds g2 = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c))));

        g1 = ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) by A12, A11;

        hence thesis by A13, A11;

      end;

    end

    theorem :: FDIFF_3:9

    

     Th9: for g be Real holds f is_left_differentiable_in x0 & ( Ldiff (f,x0)) = g iff (ex r st 0 < r & [.(x0 - r), x0.] c= ( dom f)) & for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g

    proof

      let g be Real;

      thus f is_left_differentiable_in x0 & ( Ldiff (f,x0)) = g implies (ex r st 0 < r & [.(x0 - r), x0.] c= ( dom f)) & for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g by Def5;

      thus (ex r st 0 < r & [.(x0 - r), x0.] c= ( dom f)) & (for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g) implies f is_left_differentiable_in x0 & ( Ldiff (f,x0)) = g

      proof

        assume that

         A1: ex r st 0 < r & [.(x0 - r), x0.] c= ( dom f) and

         A2: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g;

        for h, c holds ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) implies ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A2;

        hence

         A3: f is_left_differentiable_in x0 by A1;

        for h, c holds ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) implies ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g by A2;

        hence thesis by A3, Def5;

      end;

    end;

    theorem :: FDIFF_3:10

    f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies (f1 + f2) is_left_differentiable_in x0 & ( Ldiff ((f1 + f2),x0)) = (( Ldiff (f1,x0)) + ( Ldiff (f2,x0)))

    proof

      assume that

       A1: f1 is_left_differentiable_in x0 and

       A2: f2 is_left_differentiable_in x0;

      consider r2 such that

       A3: 0 < r2 and

       A4: [.(x0 - r2), x0.] c= ( dom f2) by A2;

      consider r1 such that

       A5: 0 < r1 and

       A6: [.(x0 - r1), x0.] c= ( dom f1) by A1;

      set r = ( min (r1,r2));

      

       A7: 0 < r by A5, A3, XXREAL_0: 15;

      then

       A8: (x0 - r) <= x0 by XREAL_1: 43;

      r <= r2 by XXREAL_0: 17;

      then

       A9: (x0 - r2) <= (x0 - r) by XREAL_1: 13;

      then (x0 - r2) <= x0 by A8, XXREAL_0: 2;

      then

       A10: x0 in [.(x0 - r2), x0.] by XXREAL_1: 1;

      (x0 - r) in { g : (x0 - r2) <= g & g <= x0 } by A8, A9;

      then (x0 - r) in [.(x0 - r2), x0.] by RCOMP_1:def 1;

      then [.(x0 - r), x0.] c= [.(x0 - r2), x0.] by A10, XXREAL_2:def 12;

      then

       A11: [.(x0 - r), x0.] c= ( dom f2) by A4;

      r <= r1 by XXREAL_0: 17;

      then

       A12: (x0 - r1) <= (x0 - r) by XREAL_1: 13;

      then (x0 - r1) <= x0 by A8, XXREAL_0: 2;

      then

       A13: x0 in [.(x0 - r1), x0.] by XXREAL_1: 1;

      (x0 - r) in { g : (x0 - r1) <= g & g <= x0 } by A8, A12;

      then (x0 - r) in [.(x0 - r1), x0.] by RCOMP_1:def 1;

      then [.(x0 - r), x0.] c= [.(x0 - r1), x0.] by A13, XXREAL_2:def 12;

      then [.(x0 - r), x0.] c= ( dom f1) by A6;

      then

       A14: [.(x0 - r), x0.] c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 19;

      

       A15: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f1 + f2)) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) is convergent & ( lim ((h " ) (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)))) = (( Ldiff (f1,x0)) + ( Ldiff (f2,x0)))

      proof

        let h, c;

        assume that

         A16: ( rng c) = {x0} and

         A17: ( rng (h + c)) c= ( dom (f1 + f2)) and

         A18: for n be Nat holds (h . n) < 0 ;

        

         A19: ( rng (h + c)) c= (( dom f1) /\ ( dom f2)) by A17, VALUED_1:def 1;

         A20:

        now

          let n;

          

           A21: ( rng c) c= (( dom f1) /\ ( dom f2))

          proof

            let x be object;

            assume x in ( rng c);

            then

             A22: x = x0 by A16, TARSKI:def 1;

            x0 in [.(x0 - r), x0.] by A8, XXREAL_1: 1;

            hence thesis by A14, A22;

          end;

          

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

          .= ((((f1 /* (h + c)) . n) + (( - (f1 /* c)) . n)) + (((f2 /* (h + c)) + ( - (f2 /* c))) . n)) by SEQ_1: 7

          .= ((((f1 /* (h + c)) . n) + (( - (f1 /* c)) . n)) + (((f2 /* (h + c)) . n) + (( - (f2 /* c)) . n))) by SEQ_1: 7

          .= ((((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + ((( - (f1 /* c)) . n) + (( - (f2 /* c)) . n)))

          .= ((((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + (( - ((f1 /* c) . n)) + (( - (f2 /* c)) . n))) by SEQ_1: 10

          .= ((((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + (( - ((f1 /* c) . n)) + ( - ((f2 /* c) . n)))) by SEQ_1: 10

          .= ((((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) - (((f1 /* c) . n) + ((f2 /* c) . n)))

          .= ((((f1 /* (h + c)) + (f2 /* (h + c))) . n) - (((f1 /* c) . n) + ((f2 /* c) . n))) by SEQ_1: 7

          .= ((((f1 /* (h + c)) + (f2 /* (h + c))) . n) - (((f1 /* c) + (f2 /* c)) . n)) by SEQ_1: 7

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

          .= ((((f1 + f2) /* (h + c)) - ((f1 /* c) + (f2 /* c))) . n) by A19, RFUNCT_2: 8

          .= ((((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) . n) by A21, RFUNCT_2: 8;

        end;

        then

         A23: (((f1 /* (h + c)) - (f1 /* c)) + ((f2 /* (h + c)) - (f2 /* c))) = (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) by FUNCT_2: 63;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A24: ( rng (h + c)) c= ( dom f2) by A19;

        then

         A25: ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ( Ldiff (f2,x0)) by A2, A16, A18, Th9;

        

         A26: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A16, A18, A24;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A27: ( rng (h + c)) c= ( dom f1) by A19;

        

         A28: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) + ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ((h " ) (#) (((f1 /* (h + c)) - (f1 /* c)) + ((f2 /* (h + c)) - (f2 /* c)))) by SEQ_1: 16;

        

         A29: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A16, A18, A27;

        then (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) + ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A26;

        hence ((h " ) (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) is convergent by A28, A20, FUNCT_2: 63;

        ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = ( Ldiff (f1,x0)) by A1, A16, A18, A27, Th9;

        hence thesis by A29, A26, A25, A28, A23, SEQ_2: 6;

      end;

       [.(x0 - r), x0.] c= ( dom (f1 + f2)) by A14, VALUED_1:def 1;

      hence thesis by A7, A15, Th9;

    end;

    theorem :: FDIFF_3:11

    f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies (f1 - f2) is_left_differentiable_in x0 & ( Ldiff ((f1 - f2),x0)) = (( Ldiff (f1,x0)) - ( Ldiff (f2,x0)))

    proof

      assume that

       A1: f1 is_left_differentiable_in x0 and

       A2: f2 is_left_differentiable_in x0;

      consider r2 such that

       A3: 0 < r2 and

       A4: [.(x0 - r2), x0.] c= ( dom f2) by A2;

      consider r1 such that

       A5: 0 < r1 and

       A6: [.(x0 - r1), x0.] c= ( dom f1) by A1;

      set r = ( min (r1,r2));

      

       A7: 0 < r by A5, A3, XXREAL_0: 15;

      then

       A8: (x0 - r) <= x0 by XREAL_1: 43;

      r <= r2 by XXREAL_0: 17;

      then

       A9: (x0 - r2) <= (x0 - r) by XREAL_1: 13;

      then (x0 - r2) <= x0 by A8, XXREAL_0: 2;

      then

       A10: x0 in [.(x0 - r2), x0.] by XXREAL_1: 1;

      (x0 - r) in { g : (x0 - r2) <= g & g <= x0 } by A8, A9;

      then (x0 - r) in [.(x0 - r2), x0.] by RCOMP_1:def 1;

      then [.(x0 - r), x0.] c= [.(x0 - r2), x0.] by A10, XXREAL_2:def 12;

      then

       A11: [.(x0 - r), x0.] c= ( dom f2) by A4;

      r <= r1 by XXREAL_0: 17;

      then

       A12: (x0 - r1) <= (x0 - r) by XREAL_1: 13;

      then (x0 - r1) <= x0 by A8, XXREAL_0: 2;

      then

       A13: x0 in [.(x0 - r1), x0.] by XXREAL_1: 1;

      (x0 - r) in { g : (x0 - r1) <= g & g <= x0 } by A8, A12;

      then (x0 - r) in [.(x0 - r1), x0.] by RCOMP_1:def 1;

      then [.(x0 - r), x0.] c= [.(x0 - r1), x0.] by A13, XXREAL_2:def 12;

      then [.(x0 - r), x0.] c= ( dom f1) by A6;

      then

       A14: [.(x0 - r), x0.] c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 19;

      

       A15: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f1 - f2)) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c))) is convergent & ( lim ((h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)))) = (( Ldiff (f1,x0)) - ( Ldiff (f2,x0)))

      proof

        let h, c;

        assume that

         A16: ( rng c) = {x0} and

         A17: ( rng (h + c)) c= ( dom (f1 - f2)) and

         A18: for n be Nat holds (h . n) < 0 ;

        

         A19: ( rng (h + c)) c= (( dom f1) /\ ( dom f2)) by A17, VALUED_1: 12;

         A20:

        now

          let n;

          

           A21: ( rng c) c= (( dom f1) /\ ( dom f2))

          proof

            let x be object;

            assume x in ( rng c);

            then

             A22: x = x0 by A16, TARSKI:def 1;

            x0 in [.(x0 - r), x0.] by A8, XXREAL_1: 1;

            hence thesis by A14, A22;

          end;

          

          thus ((((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c))) . n) = ((((f1 /* (h + c)) - (f1 /* c)) . n) - (((f2 /* (h + c)) - (f2 /* c)) . n)) by RFUNCT_2: 1

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

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

          .= ((((f1 /* (h + c)) . n) - ((f2 /* (h + c)) . n)) - (((f1 /* c) . n) - ((f2 /* c) . n)))

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

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

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

          .= ((((f1 - f2) /* (h + c)) - ((f1 /* c) - (f2 /* c))) . n) by A19, RFUNCT_2: 8

          .= ((((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) . n) by A21, RFUNCT_2: 8;

        end;

        then

         A23: (((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c))) = (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) by FUNCT_2: 63;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A24: ( rng (h + c)) c= ( dom f2) by A19;

        then

         A25: ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ( Ldiff (f2,x0)) by A2, A16, A18, Th9;

        

         A26: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A16, A18, A24;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A27: ( rng (h + c)) c= ( dom f1) by A19;

        

         A28: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) - ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ((h " ) (#) (((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c)))) by SEQ_1: 21;

        

         A29: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A16, A18, A27;

        then (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) - ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A26;

        hence ((h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c))) is convergent by A28, A20, FUNCT_2: 63;

        ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = ( Ldiff (f1,x0)) by A1, A16, A18, A27, Th9;

        hence thesis by A29, A26, A25, A28, A23, SEQ_2: 12;

      end;

       [.(x0 - r), x0.] c= ( dom (f1 - f2)) by A14, VALUED_1: 12;

      hence thesis by A7, A15, Th9;

    end;

    theorem :: FDIFF_3:12

    f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies (f1 (#) f2) is_left_differentiable_in x0 & ( Ldiff ((f1 (#) f2),x0)) = ((( Ldiff (f1,x0)) * (f2 . x0)) + (( Ldiff (f2,x0)) * (f1 . x0)))

    proof

      assume that

       A1: f1 is_left_differentiable_in x0 and

       A2: f2 is_left_differentiable_in x0;

      consider r2 such that

       A3: 0 < r2 and

       A4: [.(x0 - r2), x0.] c= ( dom f2) by A2;

      consider r1 such that

       A5: 0 < r1 and

       A6: [.(x0 - r1), x0.] c= ( dom f1) by A1;

      set r = ( min (r1,r2));

      

       A7: 0 < r by A5, A3, XXREAL_0: 15;

      then

       A8: (x0 - r) <= x0 by XREAL_1: 43;

      r <= r2 by XXREAL_0: 17;

      then

       A9: (x0 - r2) <= (x0 - r) by XREAL_1: 13;

      then (x0 - r2) <= x0 by A8, XXREAL_0: 2;

      then

       A10: x0 in [.(x0 - r2), x0.] by XXREAL_1: 1;

      (x0 - r) in { g : (x0 - r2) <= g & g <= x0 } by A8, A9;

      then (x0 - r) in [.(x0 - r2), x0.] by RCOMP_1:def 1;

      then [.(x0 - r), x0.] c= [.(x0 - r2), x0.] by A10, XXREAL_2:def 12;

      then

       A11: [.(x0 - r), x0.] c= ( dom f2) by A4;

      r <= r1 by XXREAL_0: 17;

      then

       A12: (x0 - r1) <= (x0 - r) by XREAL_1: 13;

      then (x0 - r1) <= x0 by A8, XXREAL_0: 2;

      then

       A13: x0 in [.(x0 - r1), x0.] by XXREAL_1: 1;

      (x0 - r) in { g : (x0 - r1) <= g & g <= x0 } by A8, A12;

      then (x0 - r) in [.(x0 - r1), x0.] by RCOMP_1:def 1;

      then [.(x0 - r), x0.] c= [.(x0 - r1), x0.] by A13, XXREAL_2:def 12;

      then

       A14: [.(x0 - r), x0.] c= ( dom f1) by A6;

      

       A15: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f1 (#) f2)) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) is convergent & ( lim ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)))) = ((( Ldiff (f1,x0)) * (f2 . x0)) + (( Ldiff (f2,x0)) * (f1 . x0)))

      proof

        let h, c;

        assume that

         A16: ( rng c) = {x0} and

         A17: ( rng (h + c)) c= ( dom (f1 (#) f2)) and

         A18: for n be Nat holds (h . n) < 0 ;

        

         A19: ( rng (h + c)) c= (( dom f1) /\ ( dom f2)) by A17, VALUED_1:def 4;

        now

          let n;

          

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

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

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

        end;

        then

         A20: ((f1 /* c) + ((f1 /* (h + c)) - (f1 /* c))) = (f1 /* (h + c)) by FUNCT_2: 63;

        

         A21: for m holds (c . m) = x0

        proof

          let m;

          (c . m) in ( rng c) by VALUED_0: 28;

          hence thesis by A16, TARSKI:def 1;

        end;

         0 <= r by A5, A3, XXREAL_0: 15;

        then (x0 - r) <= x0 by XREAL_1: 43;

        then

         A22: x0 in [.(x0 - r), x0.] by XXREAL_1: 1;

        then

         A23: x0 in ( dom f1) by A14;

        

         A24: ( rng c) c= ( dom f1) by A16, A23, TARSKI:def 1;

        

         A25: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f1 /* c) . m) - (f1 . x0)).| < g

        proof

          let g be Real such that

           A26: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A27: m in NAT by ORDINAL1:def 12;

           |.(((f1 /* c) . m) - (f1 . x0)).| = |.((f1 . (c . m)) - (f1 . x0)).| by A24, FUNCT_2: 108, A27

          .= |.((f1 . x0) - (f1 . x0)).| by A21, A27

          .= 0 by ABSVALUE:def 1;

          hence thesis by A26;

        end;

        then

         A28: (f1 /* c) is convergent by SEQ_2:def 6;

        

         A29: x0 in ( dom f2) by A11, A22;

        

         A30: ( rng c) c= ( dom f2) by A16, A29, TARSKI:def 1;

        

         A31: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f2 /* c) . m) - (f2 . x0)).| < g

        proof

          let g be Real such that

           A32: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A33: m in NAT by ORDINAL1:def 12;

           |.(((f2 /* c) . m) - (f2 . x0)).| = |.((f2 . (c . m)) - (f2 . x0)).| by A30, FUNCT_2: 108, A33

          .= |.((f2 . x0) - (f2 . x0)).| by A21, A33

          .= 0 by ABSVALUE:def 1;

          hence thesis by A32;

        end;

        then

         A34: (f2 /* c) is convergent by SEQ_2:def 6;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A35: ( rng (h + c)) c= ( dom f1) by A19;

        then

         A36: ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = ( Ldiff (f1,x0)) by A1, A16, A18, Th9;

        

         A37: h is convergent & ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A16, A18, A35;

        

        then

         A38: ( lim (h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))))) = (( lim h) * ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))))) by SEQ_2: 15

        .= 0 ;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A39: ( rng (h + c)) c= ( dom f2) by A19;

        then

         A40: ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ( Ldiff (f2,x0)) by A2, A16, A18, Th9;

        

         A41: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A16, A18, A35;

        then

         A42: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) is convergent by A34;

        

         A43: ( rng c) c= (( dom f1) /\ ( dom f2)) by A24, A30, XBOOLE_1: 19;

         A44:

        now

          let n;

          

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

          .= (((h " ) . n) * ((((f1 (#) f2) /* (h + c)) . n) - (((f1 (#) f2) /* c) . n))) by RFUNCT_2: 1

          .= (((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 (#) f2) /* c) . n))) by A19, RFUNCT_2: 8

          .= (((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 /* c) (#) (f2 /* c)) . n))) by A43, RFUNCT_2: 8

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

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

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

          .= (((((h " ) . n) * (((f2 /* (h + c)) - (f2 /* c)) . n)) * ((f1 /* (h + c)) . n)) + ((((h " ) . n) * (((f1 /* (h + c)) . n) - ((f1 /* c) . n))) * ((f2 /* c) . n))) by RFUNCT_2: 1

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

          .= (((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) . n) * ((f1 /* (h + c)) . n)) + ((((h " ) . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n))) by RFUNCT_2: 1

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

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

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

          .= (((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) . n) by SEQ_1: 7;

        end;

        then

         A45: ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = ((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by FUNCT_2: 63;

        now

          let n;

          

           A46: (h . n) <> 0 by A18;

          

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

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

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

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

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

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

        end;

        then

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

        (h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) is convergent by A37;

        then

         A48: (f1 /* (h + c)) is convergent by A28, A47, A20;

        ( lim (f1 /* c)) = (f1 . x0) by A25, A28, SEQ_2:def 7;

        then

         A49: 0 = (( lim (f1 /* (h + c))) - (f1 . x0)) by A28, A47, A48, A38, SEQ_2: 12;

        

         A50: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A16, A18, A39;

        then

         A51: (((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) is convergent by A48;

        ( lim ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)))) = ( lim ((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)))) by A44, FUNCT_2: 63

        .= (( lim (((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c)))) + ( lim (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)))) by A51, A42, SEQ_2: 6

        .= ((( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) * ( lim (f1 /* (h + c)))) + ( lim (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)))) by A50, A48, SEQ_2: 15

        .= ((( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) * (f1 . x0)) + (( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) * ( lim (f2 /* c)))) by A41, A49, A34, SEQ_2: 15

        .= ((( Ldiff (f1,x0)) * (f2 . x0)) + (( Ldiff (f2,x0)) * (f1 . x0))) by A36, A40, A31, A34, SEQ_2:def 7;

        hence thesis by A51, A42, A45;

      end;

       [.(x0 - r), x0.] c= (( dom f1) /\ ( dom f2)) by A14, A11, XBOOLE_1: 19;

      then [.(x0 - r), x0.] c= ( dom (f1 (#) f2)) by VALUED_1:def 4;

      hence thesis by A7, A15, Th9;

    end;

    

     Lm1: f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & (ex r0 st r0 > 0 & for g st g in ( dom f2) & g in [.(x0 - r0), x0.] holds (f2 . g) <> 0 ) implies (f1 / f2) is_left_differentiable_in x0 & ( Ldiff ((f1 / f2),x0)) = (((( Ldiff (f1,x0)) * (f2 . x0)) - (( Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2 ))

    proof

      assume that

       A1: f1 is_left_differentiable_in x0 and

       A2: f2 is_left_differentiable_in x0;

      consider r1 such that

       A3: 0 < r1 and

       A4: [.(x0 - r1), x0.] c= ( dom f1) by A1;

      given r0 such that

       A5: r0 > 0 and

       A6: for g st g in ( dom f2) & g in [.(x0 - r0), x0.] holds (f2 . g) <> 0 ;

      consider r2 such that

       A7: 0 < r2 and

       A8: [.(x0 - r2), x0.] c= ( dom f2) by A2;

      set r3 = ( min (r0,r2));

      

       A9: 0 < r3 by A5, A7, XXREAL_0: 15;

      then

       A10: (x0 - r3) <= x0 by XREAL_1: 43;

      r3 <= r2 by XXREAL_0: 17;

      then

       A11: (x0 - r2) <= (x0 - r3) by XREAL_1: 13;

      then (x0 - r2) <= x0 by A10, XXREAL_0: 2;

      then

       A12: x0 in [.(x0 - r2), x0.] by XXREAL_1: 1;

      (x0 - r3) in { g : (x0 - r2) <= g & g <= x0 } by A10, A11;

      then (x0 - r3) in [.(x0 - r2), x0.] by RCOMP_1:def 1;

      then [.(x0 - r3), x0.] c= [.(x0 - r2), x0.] by A12, XXREAL_2:def 12;

      then

       A13: [.(x0 - r3), x0.] c= ( dom f2) by A8;

      r3 <= r0 by XXREAL_0: 17;

      then

       A14: (x0 - r0) <= (x0 - r3) by XREAL_1: 13;

      then (x0 - r0) <= x0 by A10, XXREAL_0: 2;

      then

       A15: x0 in [.(x0 - r0), x0.] by XXREAL_1: 1;

      (x0 - r3) in { g : (x0 - r0) <= g & g <= x0 } by A10, A14;

      then (x0 - r3) in [.(x0 - r0), x0.] by RCOMP_1:def 1;

      then

       A16: [.(x0 - r3), x0.] c= [.(x0 - r0), x0.] by A15, XXREAL_2:def 12;

      set r = ( min (r1,r3));

      

       A17: 0 < r by A3, A9, XXREAL_0: 15;

      then

       A18: (x0 - r) <= x0 by XREAL_1: 43;

      r <= r3 by XXREAL_0: 17;

      then

       A19: (x0 - r3) <= (x0 - r) by XREAL_1: 13;

      then (x0 - r3) <= x0 by A18, XXREAL_0: 2;

      then

       A20: x0 in [.(x0 - r3), x0.] by XXREAL_1: 1;

      (x0 - r) in { g : (x0 - r3) <= g & g <= x0 } by A18, A19;

      then (x0 - r) in [.(x0 - r3), x0.] by RCOMP_1:def 1;

      then

       A21: [.(x0 - r), x0.] c= [.(x0 - r3), x0.] by A20, XXREAL_2:def 12;

       [.(x0 - r), x0.] c= ( dom (f2 ^ ))

      proof

        assume not thesis;

        then

        consider x be object such that

         A22: x in [.(x0 - r), x0.] and

         A23: not x in ( dom (f2 ^ ));

        reconsider x as Real by A22;

        

         A24: x in [.(x0 - r3), x0.] by A21, A22;

        

         A25: not x in (( dom f2) \ (f2 " { 0 })) by A23, RFUNCT_1:def 2;

        now

          per cases by A25, XBOOLE_0:def 5;

            suppose not x in ( dom f2);

            hence contradiction by A13, A24;

          end;

            suppose

             A26: x in (f2 " { 0 });

            then (f2 . x) in { 0 } by FUNCT_1:def 7;

            then

             A27: (f2 . x) = 0 by TARSKI:def 1;

            x in ( dom f2) by A26, FUNCT_1:def 7;

            hence contradiction by A6, A16, A24, A27;

          end;

        end;

        hence contradiction;

      end;

      then

       A28: [.(x0 - r), x0.] c= (( dom f2) \ (f2 " { 0 })) by RFUNCT_1:def 2;

      r <= r1 by XXREAL_0: 17;

      then

       A29: (x0 - r1) <= (x0 - r) by XREAL_1: 13;

      then (x0 - r1) <= x0 by A18, XXREAL_0: 2;

      then

       A30: x0 in [.(x0 - r1), x0.] by XXREAL_1: 1;

      (x0 - r) in { g : (x0 - r1) <= g & g <= x0 } by A18, A29;

      then (x0 - r) in [.(x0 - r1), x0.] by RCOMP_1:def 1;

      then [.(x0 - r), x0.] c= [.(x0 - r1), x0.] by A30, XXREAL_2:def 12;

      then

       A31: [.(x0 - r), x0.] c= ( dom f1) by A4;

      

       A32: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f1 / f2)) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) is convergent & ( lim ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)))) = (((( Ldiff (f1,x0)) * (f2 . x0)) - (( Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2 ))

      proof

        let h, c;

        assume that

         A33: ( rng c) = {x0} and

         A34: ( rng (h + c)) c= ( dom (f1 / f2)) and

         A35: for n be Nat holds (h . n) < 0 ;

        

         A36: ( rng (h + c)) c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by A34, RFUNCT_1:def 1;

         0 <= r by A3, A9, XXREAL_0: 15;

        then (x0 - r) <= x0 by XREAL_1: 43;

        then

         A37: x0 in [.(x0 - r), x0.] by XXREAL_1: 1;

        then

         A38: x0 in ( dom f1) by A31;

        

         A39: ( rng c) c= ( dom f1) by A33, A38, TARSKI:def 1;

        (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) c= ( dom f1) by XBOOLE_1: 17;

        then

         A40: ( rng (h + c)) c= ( dom f1) by A36;

        then

         A41: ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = ( Ldiff (f1,x0)) by A1, A33, A35, Th9;

        

         A42: x0 in (( dom f2) \ (f2 " { 0 })) by A28, A37;

        ( rng c) c= (( dom f2) \ (f2 " { 0 })) by A33, A42, TARSKI:def 1;

        then

         A43: ( rng c) c= ( dom (f2 ^ )) by RFUNCT_1:def 2;

        then

         A44: ( rng c) c= (( dom f1) /\ ( dom (f2 ^ ))) by A39, XBOOLE_1: 19;

        

         A45: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A33, A35, A40;

        

         A46: (f2 /* c) is non-zero by A43, RFUNCT_2: 11;

         A47:

        now

          let n;

          

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

          .= (((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* c)) . n) - (((f1 /* c) (#) (f2 /* (h + c))) . n))) by RFUNCT_2: 1

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

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

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

          .= (((((h " ) . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h " ) . n) * (((f2 /* (h + c)) . n) - ((f2 /* c) . n))))) by RFUNCT_2: 1

          .= (((((h " ) . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h " ) . n) * (((f2 /* (h + c)) - (f2 /* c)) . n)))) by RFUNCT_2: 1

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

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

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

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

          .= (((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) . n) by RFUNCT_2: 1;

        end;

        now

          let n;

          

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

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

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

        end;

        then

         A48: ((f2 /* c) + ((f2 /* (h + c)) - (f2 /* c))) = (f2 /* (h + c)) by FUNCT_2: 63;

        (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) c= (( dom f2) \ (f2 " { 0 })) by XBOOLE_1: 17;

        then

         A49: ( rng (h + c)) c= (( dom f2) \ (f2 " { 0 })) by A36;

        then

         A50: ( rng (h + c)) c= ( dom (f2 ^ )) by RFUNCT_1:def 2;

        then

         A51: ( rng (h + c)) c= (( dom f1) /\ ( dom (f2 ^ ))) by A40, XBOOLE_1: 19;

        

         A52: (f2 /* (h + c)) is non-zero by A50, RFUNCT_2: 11;

        then

         A53: ((f2 /* (h + c)) (#) (f2 /* c)) is non-zero by A46, SEQ_1: 35;

        ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = ((h " ) (#) (((f1 (#) (f2 ^ )) /* (h + c)) - ((f1 / f2) /* c))) by RFUNCT_1: 31

        .= ((h " ) (#) (((f1 (#) (f2 ^ )) /* (h + c)) - ((f1 (#) (f2 ^ )) /* c))) by RFUNCT_1: 31

        .= ((h " ) (#) (((f1 /* (h + c)) (#) ((f2 ^ ) /* (h + c))) - ((f1 (#) (f2 ^ )) /* c))) by A51, RFUNCT_2: 8

        .= ((h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 (#) (f2 ^ )) /* c))) by A50, RFUNCT_2: 12

        .= ((h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) (#) ((f2 ^ ) /* c)))) by A44, RFUNCT_2: 8

        .= ((h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) /" (f2 /* c)))) by A43, RFUNCT_2: 12

        .= ((h " ) (#) ((((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) /" ((f2 /* (h + c)) (#) (f2 /* c)))) by A52, A46, SEQ_1: 50

        .= (((h " ) (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) /" ((f2 /* (h + c)) (#) (f2 /* c))) by SEQ_1: 41;

        then

         A54: ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) /" ((f2 /* (h + c)) (#) (f2 /* c))) by A47, FUNCT_2: 63;

        (( dom f2) \ (f2 " { 0 })) c= ( dom f2) by XBOOLE_1: 36;

        then

         A55: ( rng (h + c)) c= ( dom f2) by A49;

        then

         A56: ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ( Ldiff (f2,x0)) by A2, A33, A35, Th9;

        

         A57: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A33, A35, A55;

        now

          let n;

          

           A58: (h . n) <> 0 by A35;

          

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

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

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

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

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

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

        end;

        then

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

        

         A60: for m holds (c . m) = x0

        proof

          let m;

          (c . m) in ( rng c) by VALUED_0: 28;

          hence thesis by A33, TARSKI:def 1;

        end;

        

         A61: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f1 /* c) . m) - (f1 . x0)).| < g

        proof

          let g be Real such that

           A62: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A63: m in NAT by ORDINAL1:def 12;

           |.(((f1 /* c) . m) - (f1 . x0)).| = |.((f1 . (c . m)) - (f1 . x0)).| by A39, FUNCT_2: 108, A63

          .= |.((f1 . x0) - (f1 . x0)).| by A60, A63

          .= 0 by ABSVALUE:def 1;

          hence thesis by A62;

        end;

        then

         A64: (f1 /* c) is convergent by SEQ_2:def 6;

        then

         A65: ( lim (f1 /* c)) = (f1 . x0) by A61, SEQ_2:def 7;

        ( dom (f2 ^ )) = (( dom f2) \ (f2 " { 0 })) by RFUNCT_1:def 2;

        then

         A66: ( dom (f2 ^ )) c= ( dom f2) by XBOOLE_1: 36;

        

         A67: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f2 /* c) . m) - (f2 . x0)).| < g

        proof

          let g be Real such that

           A68: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A69: m in NAT by ORDINAL1:def 12;

           |.(((f2 /* c) . m) - (f2 . x0)).| = |.((f2 . (c . m)) - (f2 . x0)).| by A43, A66, FUNCT_2: 108, XBOOLE_1: 1, A69

          .= |.((f2 . x0) - (f2 . x0)).| by A60, A69

          .= 0 by ABSVALUE:def 1;

          hence thesis by A68;

        end;

        then

         A70: (f2 /* c) is convergent by SEQ_2:def 6;

        then

         A71: ( lim (f2 /* c)) = (f2 . x0) by A67, SEQ_2:def 7;

        (h (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A57;

        then

         A72: (f2 /* (h + c)) is convergent by A70, A59, A48;

        then

         A73: ((f2 /* (h + c)) (#) (f2 /* c)) is convergent by A70;

        ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A33, A35, A55;

        

        then ( lim (h (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) = (( lim h) * ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) by SEQ_2: 15

        .= 0 ;

        then 0 = (( lim (f2 /* (h + c))) - (f2 . x0)) by A70, A71, A59, A72, SEQ_2: 12;

        then

         A74: ( lim ((f2 /* (h + c)) (#) (f2 /* c))) = ((f2 . x0) ^2 ) by A70, A71, A72, SEQ_2: 15;

        

         A75: ( lim ((f2 /* (h + c)) (#) (f2 /* c))) <> 0

        proof

          assume not thesis;

          then (f2 . x0) = 0 by A74, XCMPLX_1: 6;

          hence contradiction by A6, A8, A15, A12;

        end;

        ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A33, A35, A40;

        then

         A76: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) is convergent by A70;

        

         A77: ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A57, A64;

        then

         A78: ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) is convergent by A76;

        

        then ( lim ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)))) = (( lim ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))))) / ( lim ((f2 /* (h + c)) (#) (f2 /* c)))) by A53, A73, A75, A54, SEQ_2: 24

        .= ((( lim (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) - ( lim ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))))) / ( lim ((f2 /* (h + c)) (#) (f2 /* c)))) by A77, A76, SEQ_2: 12

        .= (((( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) * ( lim (f2 /* c))) - ( lim ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))))) / ( lim ((f2 /* (h + c)) (#) (f2 /* c)))) by A45, A70, SEQ_2: 15

        .= (((( Ldiff (f1,x0)) * (f2 . x0)) - (( Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2 )) by A41, A57, A56, A64, A65, A71, A74, SEQ_2: 15;

        hence thesis by A53, A73, A75, A78, A54, SEQ_2: 23;

      end;

       [.(x0 - r), x0.] c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by A31, A28, XBOOLE_1: 19;

      then [.(x0 - r), x0.] c= ( dom (f1 / f2)) by RFUNCT_1:def 1;

      hence thesis by A17, A32, Th9;

    end;

    theorem :: FDIFF_3:13

    f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 & (f2 . x0) <> 0 implies (f1 / f2) is_left_differentiable_in x0 & ( Ldiff ((f1 / f2),x0)) = (((( Ldiff (f1,x0)) * (f2 . x0)) - (( Ldiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2 ))

    proof

      assume that

       A1: f1 is_left_differentiable_in x0 and

       A2: f2 is_left_differentiable_in x0 and

       A3: (f2 . x0) <> 0 ;

      consider r1 such that

       A4: r1 > 0 and [.(x0 - r1), x0.] c= ( dom f2) and

       A5: for g st g in [.(x0 - r1), x0.] holds (f2 . g) <> 0 by A2, A3, Th5, Th6;

      now

        take r1;

        thus r1 > 0 by A4;

        let g;

        assume that g in ( dom f2) and

         A6: g in [.(x0 - r1), x0.];

        thus (f2 . g) <> 0 by A5, A6;

      end;

      hence thesis by A1, A2, Lm1;

    end;

    

     Lm2: f is_left_differentiable_in x0 & (ex r0 st r0 > 0 & for g st g in ( dom f) & g in [.(x0 - r0), x0.] holds (f . g) <> 0 ) implies (f ^ ) is_left_differentiable_in x0 & ( Ldiff ((f ^ ),x0)) = ( - (( Ldiff (f,x0)) / ((f . x0) ^2 )))

    proof

      assume

       A1: f is_left_differentiable_in x0;

      then

      consider r2 such that

       A2: 0 < r2 and

       A3: [.(x0 - r2), x0.] c= ( dom f);

      given r0 such that

       A4: r0 > 0 and

       A5: for g st g in ( dom f) & g in [.(x0 - r0), x0.] holds (f . g) <> 0 ;

      set r3 = ( min (r0,r2));

      

       A6: 0 < r3 by A4, A2, XXREAL_0: 15;

      then

       A7: (x0 - r3) <= x0 by XREAL_1: 43;

      r3 <= r2 by XXREAL_0: 17;

      then

       A8: (x0 - r2) <= (x0 - r3) by XREAL_1: 13;

      then (x0 - r2) <= x0 by A7, XXREAL_0: 2;

      then

       A9: x0 in [.(x0 - r2), x0.] by XXREAL_1: 1;

      (x0 - r3) in { g : (x0 - r2) <= g & g <= x0 } by A7, A8;

      then (x0 - r3) in [.(x0 - r2), x0.] by RCOMP_1:def 1;

      then [.(x0 - r3), x0.] c= [.(x0 - r2), x0.] by A9, XXREAL_2:def 12;

      then

       A10: [.(x0 - r3), x0.] c= ( dom f) by A3;

      r3 <= r0 by XXREAL_0: 17;

      then

       A11: (x0 - r0) <= (x0 - r3) by XREAL_1: 13;

      then (x0 - r0) <= x0 by A7, XXREAL_0: 2;

      then

       A12: x0 in [.(x0 - r0), x0.] by XXREAL_1: 1;

      (x0 - r3) in { g : (x0 - r0) <= g & g <= x0 } by A7, A11;

      then (x0 - r3) in [.(x0 - r0), x0.] by RCOMP_1:def 1;

      then

       A13: [.(x0 - r3), x0.] c= [.(x0 - r0), x0.] by A12, XXREAL_2:def 12;

      

       A14: [.(x0 - r3), x0.] c= ( dom (f ^ ))

      proof

        assume not thesis;

        then

        consider x be object such that

         A15: x in [.(x0 - r3), x0.] and

         A16: not x in ( dom (f ^ ));

        reconsider x as Real by A15;

        

         A17: not x in (( dom f) \ (f " { 0 })) by A16, RFUNCT_1:def 2;

        now

          per cases by A17, XBOOLE_0:def 5;

            suppose not x in ( dom f);

            hence contradiction by A10, A15;

          end;

            suppose

             A18: x in (f " { 0 });

            then (f . x) in { 0 } by FUNCT_1:def 7;

            then

             A19: (f . x) = 0 by TARSKI:def 1;

            x in ( dom f) by A18, FUNCT_1:def 7;

            hence contradiction by A5, A13, A15, A19;

          end;

        end;

        hence contradiction;

      end;

      

       A20: x0 in [.(x0 - r3), x0.] by A7, XXREAL_1: 1;

      for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f ^ )) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) is convergent & ( lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)))) = ( - (( Ldiff (f,x0)) / ((f . x0) ^2 )))

      proof

        let h, c;

        assume that

         A21: ( rng c) = {x0} and

         A22: ( rng (h + c)) c= ( dom (f ^ )) and

         A23: for n be Nat holds (h . n) < 0 ;

        

         A24: for m holds (c . m) = x0

        proof

          let m;

          (c . m) in ( rng c) by VALUED_0: 28;

          hence thesis by A21, TARSKI:def 1;

        end;

        

         A25: (( dom f) \ (f " { 0 })) c= ( dom f) by XBOOLE_1: 36;

        ( rng (h + c)) c= (( dom f) \ (f " { 0 })) by A22, RFUNCT_1:def 2;

        then

         A26: ( rng (h + c)) c= ( dom f) by A25;

        then

         A27: ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ( Ldiff (f,x0)) by A1, A21, A23, Th9;

        

         A28: ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A1, A21, A23, A26;

        then

         A29: ( - ((h " ) (#) ((f /* (h + c)) - (f /* c)))) is convergent;

        x0 in ( dom (f ^ )) by A20, A14;

        then

         A30: x0 in (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

        ( rng c) c= (( dom f) \ (f " { 0 })) by A21, A30, TARSKI:def 1;

        then

         A31: ( rng c) c= ( dom (f ^ )) by RFUNCT_1:def 2;

        then

         A32: (f /* c) is non-zero by RFUNCT_2: 11;

        now

          let n;

          

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

          

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

          .= (((h (#) (h " )) . n) * (((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

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

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

        end;

        then

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

        

         A35: (f /* (h + c)) is non-zero by A22, RFUNCT_2: 11;

        then

         A36: ((f /* (h + c)) (#) (f /* c)) is non-zero by A32, SEQ_1: 35;

        now

          let n;

          

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

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

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

        end;

        then

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

        ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

        then

         A38: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

        

         A39: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f /* c) . m) - (f . x0)).| < g

        proof

          let g be Real such that

           A40: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A41: m in NAT by ORDINAL1:def 12;

           |.(((f /* c) . m) - (f . x0)).| = |.((f . (c . m)) - (f . x0)).| by A31, A38, FUNCT_2: 108, XBOOLE_1: 1, A41

          .= |.((f . x0) - (f . x0)).| by A24, A41

          .= 0 by ABSVALUE:def 1;

          hence thesis by A40;

        end;

        then

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

        then

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

        (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) is convergent by A28;

        then

         A44: (f /* (h + c)) is convergent by A42, A34, A37;

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

        .= 0 ;

        then 0 = (( lim (f /* (h + c))) - (f . x0)) by A42, A43, A34, A44, SEQ_2: 12;

        then

         A45: ( lim ((f /* (h + c)) (#) (f /* c))) = ((f . x0) ^2 ) by A42, A43, A44, SEQ_2: 15;

        

         A46: ( lim ((f /* (h + c)) (#) (f /* c))) <> 0

        proof

          assume not thesis;

          then (f . x0) = 0 by A45, XCMPLX_1: 6;

          hence contradiction by A5, A3, A12, A9;

        end;

        now

          let n;

          

           A47: ((f /* (h + c)) . n) <> 0 & ((f /* c) . n) <> 0 by A35, A32, SEQ_1: 5;

          

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

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

          .= (((h " ) . n) * ((((f /* (h + c)) " ) . n) - (((f ^ ) /* c) . n))) by A22, RFUNCT_2: 12

          .= (((h " ) . n) * ((((f /* (h + c)) " ) . n) - (((f /* c) " ) . n))) by A31, RFUNCT_2: 12

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

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

          .= (((h " ) . n) * ((1 / ((f /* (h + c)) . n)) - (((f /* c) . n) " ))) by XCMPLX_1: 215

          .= (((h " ) . n) * ((1 / ((f /* (h + c)) . n)) - (1 / ((f /* c) . n)))) by XCMPLX_1: 215

          .= (((h " ) . n) * (((1 * ((f /* c) . n)) - (1 * ((f /* (h + c)) . n))) / (((f /* (h + c)) . n) * ((f /* c) . n)))) by A47, XCMPLX_1: 130

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

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

          .= (((h " ) . n) * ( - ((((f /* (h + c)) - (f /* c)) . n) / (((f /* (h + c)) (#) (f /* c)) . n)))) by XCMPLX_1: 187

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

          .= ( - ((((h " ) . n) * (((f /* (h + c)) - (f /* c)) . n)) / (((f /* (h + c)) (#) (f /* c)) . n))) by XCMPLX_1: 74

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

          .= ( - ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . n) * ((((f /* (h + c)) (#) (f /* c)) . n) " ))) by XCMPLX_0:def 9

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

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

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

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

        end;

        then

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

        

         A49: ((f /* (h + c)) (#) (f /* c)) is convergent by A42, A44;

        

        then ( lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)))) = (( lim ( - ((h " ) (#) ((f /* (h + c)) - (f /* c))))) / ((f . x0) ^2 )) by A36, A45, A46, A29, A48, SEQ_2: 24

        .= (( - ( Ldiff (f,x0))) / ((f . x0) ^2 )) by A28, A27, SEQ_2: 10

        .= ( - (( Ldiff (f,x0)) / ((f . x0) ^2 ))) by XCMPLX_1: 187;

        hence thesis by A36, A49, A46, A29, A48, SEQ_2: 23;

      end;

      hence thesis by A6, A14, Th9;

    end;

    theorem :: FDIFF_3:14

    f is_left_differentiable_in x0 & (f . x0) <> 0 implies (f ^ ) is_left_differentiable_in x0 & ( Ldiff ((f ^ ),x0)) = ( - (( Ldiff (f,x0)) / ((f . x0) ^2 )))

    proof

      assume that

       A1: f is_left_differentiable_in x0 and

       A2: (f . x0) <> 0 ;

      consider r1 such that

       A3: r1 > 0 and [.(x0 - r1), x0.] c= ( dom f) and

       A4: for g st g in [.(x0 - r1), x0.] holds (f . g) <> 0 by A1, A2, Th5, Th6;

      now

        take r1;

        thus r1 > 0 by A3;

        let g;

        assume that g in ( dom f) and

         A5: g in [.(x0 - r1), x0.];

        thus (f . g) <> 0 by A4, A5;

      end;

      hence thesis by A1, Lm2;

    end;

    theorem :: FDIFF_3:15

    

     Th15: for g1 be Real holds f is_right_differentiable_in x0 & ( Rdiff (f,x0)) = g1 iff (ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f)) & for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g1

    proof

      let g1 be Real;

      thus f is_right_differentiable_in x0 & ( Rdiff (f,x0)) = g1 implies (ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f)) & for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g1 by Def6;

      assume that

       A1: ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f) and

       A2: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g1;

      for h, c holds (( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & for n be Nat holds (h . n) > 0 ) implies ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A2;

      hence

       A3: f is_right_differentiable_in x0 by A1;

      for h, c holds (( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & for n be Nat holds (h . n) > 0 ) implies ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = g1 by A2;

      hence thesis by A3, Def6;

    end;

    theorem :: FDIFF_3:16

    f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 implies (f1 + f2) is_right_differentiable_in x0 & ( Rdiff ((f1 + f2),x0)) = (( Rdiff (f1,x0)) + ( Rdiff (f2,x0)))

    proof

      assume that

       A1: f1 is_right_differentiable_in x0 and

       A2: f2 is_right_differentiable_in x0;

      consider r2 such that

       A3: r2 > 0 and

       A4: [.x0, (x0 + r2).] c= ( dom f2) by A2;

      consider r1 such that

       A5: r1 > 0 and

       A6: [.x0, (x0 + r1).] c= ( dom f1) by A1;

      

       A7: (x0 + 0 ) = x0;

      set r = ( min (r1,r2));

       0 <= r by A5, A3, XXREAL_0: 15;

      then

       A8: x0 <= (x0 + r) by A7, XREAL_1: 7;

      r <= r2 by XXREAL_0: 17;

      then

       A9: (x0 + r) <= (x0 + r2) by XREAL_1: 7;

      then (x0 + r) in { g : x0 <= g & g <= (x0 + r2) } by A8;

      then

       A10: (x0 + r) in [.x0, (x0 + r2).] by RCOMP_1:def 1;

      x0 <= (x0 + r2) by A8, A9, XXREAL_0: 2;

      then x0 in [.x0, (x0 + r2).] by XXREAL_1: 1;

      then [.x0, (x0 + r).] c= [.x0, (x0 + r2).] by A10, XXREAL_2:def 12;

      then

       A11: [.x0, (x0 + r).] c= ( dom f2) by A4;

      r <= r1 by XXREAL_0: 17;

      then

       A12: (x0 + r) <= (x0 + r1) by XREAL_1: 7;

      then (x0 + r) in { g : x0 <= g & g <= (x0 + r1) } by A8;

      then

       A13: (x0 + r) in [.x0, (x0 + r1).] by RCOMP_1:def 1;

      x0 <= (x0 + r1) by A12, A8, XXREAL_0: 2;

      then x0 in [.x0, (x0 + r1).] by XXREAL_1: 1;

      then [.x0, (x0 + r).] c= [.x0, (x0 + r1).] by A13, XXREAL_2:def 12;

      then [.x0, (x0 + r).] c= ( dom f1) by A6;

      then

       A14: [.x0, (x0 + r).] c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 19;

      then

       A15: [.x0, (x0 + r).] c= ( dom (f1 + f2)) by VALUED_1:def 1;

      

       A16: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f1 + f2)) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) is convergent & ( lim ((h " ) (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)))) = (( Rdiff (f1,x0)) + ( Rdiff (f2,x0)))

      proof

        let h, c;

        assume that

         A17: ( rng c) = {x0} and

         A18: ( rng (h + c)) c= ( dom (f1 + f2)) and

         A19: for n be Nat holds (h . n) > 0 ;

        

         A20: ( rng (h + c)) c= (( dom f1) /\ ( dom f2)) by A18, VALUED_1:def 1;

         A21:

        now

          let n;

          

           A22: ( rng c) c= (( dom f1) /\ ( dom f2))

          proof

            let x be object;

            assume x in ( rng c);

            then

             A23: x = x0 by A17, TARSKI:def 1;

            x0 in [.x0, (x0 + r).] by A8, XXREAL_1: 1;

            hence thesis by A14, A23;

          end;

          

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

          .= ((((f1 /* (h + c)) . n) + (( - (f1 /* c)) . n)) + (((f2 /* (h + c)) + ( - (f2 /* c))) . n)) by SEQ_1: 7

          .= ((((f1 /* (h + c)) . n) + (( - (f1 /* c)) . n)) + (((f2 /* (h + c)) . n) + (( - (f2 /* c)) . n))) by SEQ_1: 7

          .= ((((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + ((( - (f1 /* c)) . n) + (( - (f2 /* c)) . n)))

          .= ((((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + (( - ((f1 /* c) . n)) + (( - (f2 /* c)) . n))) by SEQ_1: 10

          .= ((((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) + (( - ((f1 /* c) . n)) + ( - ((f2 /* c) . n)))) by SEQ_1: 10

          .= ((((f1 /* (h + c)) . n) + ((f2 /* (h + c)) . n)) - (((f1 /* c) . n) + ((f2 /* c) . n)))

          .= ((((f1 /* (h + c)) + (f2 /* (h + c))) . n) - (((f1 /* c) . n) + ((f2 /* c) . n))) by SEQ_1: 7

          .= ((((f1 /* (h + c)) + (f2 /* (h + c))) . n) - (((f1 /* c) + (f2 /* c)) . n)) by SEQ_1: 7

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

          .= ((((f1 + f2) /* (h + c)) - ((f1 /* c) + (f2 /* c))) . n) by A20, RFUNCT_2: 8

          .= ((((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) . n) by A22, RFUNCT_2: 8;

        end;

        then

         A24: (((f1 /* (h + c)) - (f1 /* c)) + ((f2 /* (h + c)) - (f2 /* c))) = (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c)) by FUNCT_2: 63;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A25: ( rng (h + c)) c= ( dom f2) by A20;

        then

         A26: ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ( Rdiff (f2,x0)) by A2, A17, A19, Th15;

        

         A27: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A17, A19, A25;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A28: ( rng (h + c)) c= ( dom f1) by A20;

        

         A29: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) + ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ((h " ) (#) (((f1 /* (h + c)) - (f1 /* c)) + ((f2 /* (h + c)) - (f2 /* c)))) by SEQ_1: 16;

        

         A30: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A17, A19, A28;

        then (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) + ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A27;

        hence ((h " ) (#) (((f1 + f2) /* (h + c)) - ((f1 + f2) /* c))) is convergent by A29, A21, FUNCT_2: 63;

        ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = ( Rdiff (f1,x0)) by A1, A17, A19, A28, Th15;

        hence thesis by A30, A27, A26, A29, A24, SEQ_2: 6;

      end;

       0 < r by A5, A3, XXREAL_0: 15;

      hence thesis by A15, A16, Th15;

    end;

    theorem :: FDIFF_3:17

    f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 implies (f1 - f2) is_right_differentiable_in x0 & ( Rdiff ((f1 - f2),x0)) = (( Rdiff (f1,x0)) - ( Rdiff (f2,x0)))

    proof

      assume that

       A1: f1 is_right_differentiable_in x0 and

       A2: f2 is_right_differentiable_in x0;

      consider r2 such that

       A3: r2 > 0 and

       A4: [.x0, (x0 + r2).] c= ( dom f2) by A2;

      consider r1 such that

       A5: r1 > 0 and

       A6: [.x0, (x0 + r1).] c= ( dom f1) by A1;

      set r = ( min (r1,r2));

      

       A7: 0 < r by A5, A3, XXREAL_0: 15;

      then

       A8: (x0 + 0 ) <= (x0 + r) by XREAL_1: 7;

      r <= r2 by XXREAL_0: 17;

      then

       A9: (x0 + r) <= (x0 + r2) by XREAL_1: 7;

      then (x0 + r) in { g : x0 <= g & g <= (x0 + r2) } by A8;

      then

       A10: (x0 + r) in [.x0, (x0 + r2).] by RCOMP_1:def 1;

      x0 <= (x0 + r2) by A8, A9, XXREAL_0: 2;

      then x0 in [.x0, (x0 + r2).] by XXREAL_1: 1;

      then [.x0, (x0 + r).] c= [.x0, (x0 + r2).] by A10, XXREAL_2:def 12;

      then

       A11: [.x0, (x0 + r).] c= ( dom f2) by A4;

      r <= r1 by XXREAL_0: 17;

      then

       A12: (x0 + r) <= (x0 + r1) by XREAL_1: 7;

      then (x0 + r) in { g : x0 <= g & g <= (x0 + r1) } by A8;

      then

       A13: (x0 + r) in [.x0, (x0 + r1).] by RCOMP_1:def 1;

      x0 <= (x0 + r1) by A12, A8, XXREAL_0: 2;

      then x0 in [.x0, (x0 + r1).] by XXREAL_1: 1;

      then [.x0, (x0 + r).] c= [.x0, (x0 + r1).] by A13, XXREAL_2:def 12;

      then [.x0, (x0 + r).] c= ( dom f1) by A6;

      then

       A14: [.x0, (x0 + r).] c= (( dom f1) /\ ( dom f2)) by A11, XBOOLE_1: 19;

      

       A15: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f1 - f2)) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c))) is convergent & ( lim ((h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)))) = (( Rdiff (f1,x0)) - ( Rdiff (f2,x0)))

      proof

        let h, c;

        assume that

         A16: ( rng c) = {x0} and

         A17: ( rng (h + c)) c= ( dom (f1 - f2)) and

         A18: for n be Nat holds (h . n) > 0 ;

        

         A19: ( rng (h + c)) c= (( dom f1) /\ ( dom f2)) by A17, VALUED_1: 12;

         A20:

        now

          let n;

          

           A21: ( rng c) c= (( dom f1) /\ ( dom f2))

          proof

            let x be object;

            assume x in ( rng c);

            then

             A22: x = x0 by A16, TARSKI:def 1;

            x0 in [.x0, (x0 + r).] by A8, XXREAL_1: 1;

            hence thesis by A14, A22;

          end;

          

          thus ((((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c))) . n) = ((((f1 /* (h + c)) - (f1 /* c)) . n) - (((f2 /* (h + c)) - (f2 /* c)) . n)) by RFUNCT_2: 1

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

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

          .= ((((f1 /* (h + c)) . n) - ((f2 /* (h + c)) . n)) - (((f1 /* c) . n) - ((f2 /* c) . n)))

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

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

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

          .= ((((f1 - f2) /* (h + c)) - ((f1 /* c) - (f2 /* c))) . n) by A19, RFUNCT_2: 8

          .= ((((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) . n) by A21, RFUNCT_2: 8;

        end;

        then

         A23: (((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c))) = (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c)) by FUNCT_2: 63;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A24: ( rng (h + c)) c= ( dom f2) by A19;

        then

         A25: ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ( Rdiff (f2,x0)) by A2, A16, A18, Th15;

        

         A26: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A16, A18, A24;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A27: ( rng (h + c)) c= ( dom f1) by A19;

        

         A28: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) - ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ((h " ) (#) (((f1 /* (h + c)) - (f1 /* c)) - ((f2 /* (h + c)) - (f2 /* c)))) by SEQ_1: 21;

        

         A29: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A16, A18, A27;

        then (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) - ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A26;

        hence ((h " ) (#) (((f1 - f2) /* (h + c)) - ((f1 - f2) /* c))) is convergent by A28, A20, FUNCT_2: 63;

        ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = ( Rdiff (f1,x0)) by A1, A16, A18, A27, Th15;

        hence thesis by A29, A26, A25, A28, A23, SEQ_2: 12;

      end;

       [.x0, (x0 + r).] c= ( dom (f1 - f2)) by A14, VALUED_1: 12;

      hence thesis by A7, A15, Th15;

    end;

    theorem :: FDIFF_3:18

    f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 implies (f1 (#) f2) is_right_differentiable_in x0 & ( Rdiff ((f1 (#) f2),x0)) = ((( Rdiff (f1,x0)) * (f2 . x0)) + (( Rdiff (f2,x0)) * (f1 . x0)))

    proof

      assume that

       A1: f1 is_right_differentiable_in x0 and

       A2: f2 is_right_differentiable_in x0;

      

       A3: (x0 + 0 ) = x0;

      consider r2 such that

       A4: r2 > 0 and

       A5: [.x0, (x0 + r2).] c= ( dom f2) by A2;

      consider r1 such that

       A6: r1 > 0 and

       A7: [.x0, (x0 + r1).] c= ( dom f1) by A1;

      set r = ( min (r1,r2));

       0 <= r by A6, A4, XXREAL_0: 15;

      then

       A8: x0 <= (x0 + r) by A3, XREAL_1: 7;

      r <= r2 by XXREAL_0: 17;

      then

       A9: (x0 + r) <= (x0 + r2) by XREAL_1: 7;

      then (x0 + r) in { g : x0 <= g & g <= (x0 + r2) } by A8;

      then

       A10: (x0 + r) in [.x0, (x0 + r2).] by RCOMP_1:def 1;

      x0 <= (x0 + r2) by A8, A9, XXREAL_0: 2;

      then x0 in [.x0, (x0 + r2).] by XXREAL_1: 1;

      then [.x0, (x0 + r).] c= [.x0, (x0 + r2).] by A10, XXREAL_2:def 12;

      then

       A11: [.x0, (x0 + r).] c= ( dom f2) by A5;

      r <= r1 by XXREAL_0: 17;

      then

       A12: (x0 + r) <= (x0 + r1) by XREAL_1: 7;

      then (x0 + r) in { g : x0 <= g & g <= (x0 + r1) } by A8;

      then

       A13: (x0 + r) in [.x0, (x0 + r1).] by RCOMP_1:def 1;

      x0 <= (x0 + r1) by A12, A8, XXREAL_0: 2;

      then x0 in [.x0, (x0 + r1).] by XXREAL_1: 1;

      then [.x0, (x0 + r).] c= [.x0, (x0 + r1).] by A13, XXREAL_2:def 12;

      then

       A14: [.x0, (x0 + r).] c= ( dom f1) by A7;

      

       A15: 0 < r by A6, A4, XXREAL_0: 15;

      

       A16: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f1 (#) f2)) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) is convergent & ( lim ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)))) = ((( Rdiff (f1,x0)) * (f2 . x0)) + (( Rdiff (f2,x0)) * (f1 . x0)))

      proof

        let h, c;

        assume that

         A17: ( rng c) = {x0} and

         A18: ( rng (h + c)) c= ( dom (f1 (#) f2)) and

         A19: for n be Nat holds (h . n) > 0 ;

        

         A20: ( rng (h + c)) c= (( dom f1) /\ ( dom f2)) by A18, VALUED_1:def 4;

        (x0 + 0 ) <= (x0 + r) by A15, XREAL_1: 7;

        then

         A21: x0 in [.x0, (x0 + r).] by XXREAL_1: 1;

        then

         A22: x0 in ( dom f2) by A11;

        

         A23: ( rng c) c= ( dom f2) by A17, A22, TARSKI:def 1;

        

         A24: for m holds (c . m) = x0

        proof

          let m;

          (c . m) in ( rng c) by VALUED_0: 28;

          hence thesis by A17, TARSKI:def 1;

        end;

        

         A25: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f2 /* c) . m) - (f2 . x0)).| < g

        proof

          let g be Real such that

           A26: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A27: m in NAT by ORDINAL1:def 12;

           |.(((f2 /* c) . m) - (f2 . x0)).| = |.((f2 . (c . m)) - (f2 . x0)).| by A23, FUNCT_2: 108, A27

          .= |.((f2 . x0) - (f2 . x0)).| by A24, A27

          .= 0 by ABSVALUE:def 1;

          hence thesis by A26;

        end;

        then

         A28: (f2 /* c) is convergent by SEQ_2:def 6;

        (( dom f1) /\ ( dom f2)) c= ( dom f2) by XBOOLE_1: 17;

        then

         A29: ( rng (h + c)) c= ( dom f2) by A20;

        then

         A30: ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ( Rdiff (f2,x0)) by A2, A17, A19, Th15;

        now

          let n;

          

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

          

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

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

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

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

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

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

        end;

        then

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

        

         A33: x0 in ( dom f1) by A14, A21;

        

         A34: ( rng c) c= ( dom f1) by A17, A33, TARSKI:def 1;

        

         A35: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f1 /* c) . m) - (f1 . x0)).| < g

        proof

          let g be Real such that

           A36: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A37: m in NAT by ORDINAL1:def 12;

           |.(((f1 /* c) . m) - (f1 . x0)).| = |.((f1 . (c . m)) - (f1 . x0)).| by A34, FUNCT_2: 108, A37

          .= |.((f1 . x0) - (f1 . x0)).| by A24, A37

          .= 0 by ABSVALUE:def 1;

          hence thesis by A36;

        end;

        then

         A38: (f1 /* c) is convergent by SEQ_2:def 6;

        (( dom f1) /\ ( dom f2)) c= ( dom f1) by XBOOLE_1: 17;

        then

         A39: ( rng (h + c)) c= ( dom f1) by A20;

        then

         A40: ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = ( Rdiff (f1,x0)) by A1, A17, A19, Th15;

        

         A41: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A17, A19, A39;

        then

         A42: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) is convergent by A28;

        

         A43: ( rng c) c= (( dom f1) /\ ( dom f2)) by A34, A23, XBOOLE_1: 19;

         A44:

        now

          let n;

          

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

          .= (((h " ) . n) * ((((f1 (#) f2) /* (h + c)) . n) - (((f1 (#) f2) /* c) . n))) by RFUNCT_2: 1

          .= (((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 (#) f2) /* c) . n))) by A20, RFUNCT_2: 8

          .= (((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 /* c) (#) (f2 /* c)) . n))) by A43, RFUNCT_2: 8

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

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

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

          .= (((((h " ) . n) * (((f2 /* (h + c)) - (f2 /* c)) . n)) * ((f1 /* (h + c)) . n)) + ((((h " ) . n) * (((f1 /* (h + c)) . n) - ((f1 /* c) . n))) * ((f2 /* c) . n))) by RFUNCT_2: 1

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

          .= (((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) . n) * ((f1 /* (h + c)) . n)) + ((((h " ) . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n))) by RFUNCT_2: 1

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

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

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

          .= (((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) . n) by SEQ_1: 7;

        end;

        then

         A45: ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = ((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by FUNCT_2: 63;

        now

          let n;

          

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

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

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

        end;

        then

         A46: ((f1 /* c) + ((f1 /* (h + c)) - (f1 /* c))) = (f1 /* (h + c)) by FUNCT_2: 63;

        

         A47: h is convergent & ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A17, A19, A39;

        then (h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) is convergent;

        then

         A48: (f1 /* (h + c)) is convergent by A38, A32, A46;

        ( lim (h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))))) = (( lim h) * ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))))) by A47, SEQ_2: 15

        .= 0 ;

        

        then

         A49: 0 = (( lim (f1 /* (h + c))) - ( lim (f1 /* c))) by A38, A32, A48, SEQ_2: 12

        .= (( lim (f1 /* (h + c))) - (f1 . x0)) by A35, A38, SEQ_2:def 7;

        

         A50: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A17, A19, A29;

        then

         A51: (((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) is convergent by A48;

        ( lim ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)))) = ( lim ((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)))) by A44, FUNCT_2: 63

        .= (( lim (((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c)))) + ( lim (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)))) by A51, A42, SEQ_2: 6

        .= ((( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) * ( lim (f1 /* (h + c)))) + ( lim (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)))) by A50, A48, SEQ_2: 15

        .= ((( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) * (f1 . x0)) + (( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) * ( lim (f2 /* c)))) by A41, A49, A28, SEQ_2: 15

        .= ((( Rdiff (f1,x0)) * (f2 . x0)) + (( Rdiff (f2,x0)) * (f1 . x0))) by A40, A30, A25, A28, SEQ_2:def 7;

        hence thesis by A51, A42, A45;

      end;

       [.x0, (x0 + r).] c= (( dom f1) /\ ( dom f2)) by A14, A11, XBOOLE_1: 19;

      then [.x0, (x0 + r).] c= ( dom (f1 (#) f2)) by VALUED_1:def 4;

      hence thesis by A15, A16, Th15;

    end;

    

     Lm3: f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & (ex r0 st r0 > 0 & for g st g in ( dom f2) & g in [.x0, (x0 + r0).] holds (f2 . g) <> 0 ) implies (f1 / f2) is_right_differentiable_in x0 & ( Rdiff ((f1 / f2),x0)) = (((( Rdiff (f1,x0)) * (f2 . x0)) - (( Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2 ))

    proof

      assume that

       A1: f1 is_right_differentiable_in x0 and

       A2: f2 is_right_differentiable_in x0;

      consider r2 such that

       A3: 0 < r2 and

       A4: [.x0, (x0 + r2).] c= ( dom f2) by A2;

      consider r1 such that

       A5: 0 < r1 and

       A6: [.x0, (x0 + r1).] c= ( dom f1) by A1;

      given r0 such that

       A7: r0 > 0 and

       A8: for g st g in ( dom f2) & g in [.x0, (x0 + r0).] holds (f2 . g) <> 0 ;

      

       A9: ( 0 + x0) = x0;

      set r3 = ( min (r0,r2));

       0 <= r3 by A7, A3, XXREAL_0: 15;

      then

       A10: x0 <= (x0 + r3) by A9, XREAL_1: 6;

      r3 <= r2 by XXREAL_0: 17;

      then

       A11: (x0 + r3) <= (x0 + r2) by XREAL_1: 7;

      then x0 <= (x0 + r2) by A10, XXREAL_0: 2;

      then

       A12: x0 in [.x0, (x0 + r2).] by XXREAL_1: 1;

      (x0 + r3) in { g : x0 <= g & g <= (x0 + r2) } by A10, A11;

      then (x0 + r3) in [.x0, (x0 + r2).] by RCOMP_1:def 1;

      then [.x0, (x0 + r3).] c= [.x0, (x0 + r2).] by A12, XXREAL_2:def 12;

      then

       A13: [.x0, (x0 + r3).] c= ( dom f2) by A4;

      r3 <= r0 by XXREAL_0: 17;

      then

       A14: (x0 + r3) <= (x0 + r0) by XREAL_1: 7;

      then x0 <= (x0 + r0) by A10, XXREAL_0: 2;

      then

       A15: x0 in [.x0, (x0 + r0).] by XXREAL_1: 1;

      

       A16: (x0 + 0 ) = x0;

      set r = ( min (r1,r3));

      

       A17: 0 < r3 by A7, A3, XXREAL_0: 15;

      then 0 <= r by A5, XXREAL_0: 15;

      then

       A18: x0 <= (x0 + r) by A16, XREAL_1: 7;

      r <= r3 by XXREAL_0: 17;

      then

       A19: (x0 + r) <= (x0 + r3) by XREAL_1: 7;

      then x0 <= (x0 + r3) by A18, XXREAL_0: 2;

      then

       A20: x0 in [.x0, (x0 + r3).] by XXREAL_1: 1;

      (x0 + r3) in { g : x0 <= g & g <= (x0 + r0) } by A10, A14;

      then (x0 + r3) in [.x0, (x0 + r0).] by RCOMP_1:def 1;

      then

       A21: [.x0, (x0 + r3).] c= [.x0, (x0 + r0).] by A15, XXREAL_2:def 12;

      (x0 + r) in { g : x0 <= g & g <= (x0 + r3) } by A18, A19;

      then (x0 + r) in [.x0, (x0 + r3).] by RCOMP_1:def 1;

      then

       A22: [.x0, (x0 + r).] c= [.x0, (x0 + r3).] by A20, XXREAL_2:def 12;

       [.x0, (x0 + r).] c= ( dom (f2 ^ ))

      proof

        assume not thesis;

        then

        consider x be object such that

         A23: x in [.x0, (x0 + r).] and

         A24: not x in ( dom (f2 ^ ));

        reconsider x as Real by A23;

        

         A25: x in [.x0, (x0 + r3).] by A22, A23;

        

         A26: not x in (( dom f2) \ (f2 " { 0 })) by A24, RFUNCT_1:def 2;

        now

          per cases by A26, XBOOLE_0:def 5;

            suppose not x in ( dom f2);

            hence contradiction by A13, A25;

          end;

            suppose

             A27: x in (f2 " { 0 });

            then (f2 . x) in { 0 } by FUNCT_1:def 7;

            then

             A28: (f2 . x) = 0 by TARSKI:def 1;

            x in ( dom f2) by A27, FUNCT_1:def 7;

            hence contradiction by A8, A21, A25, A28;

          end;

        end;

        hence contradiction;

      end;

      then

       A29: [.x0, (x0 + r).] c= (( dom f2) \ (f2 " { 0 })) by RFUNCT_1:def 2;

      r <= r1 by XXREAL_0: 17;

      then

       A30: (x0 + r) <= (x0 + r1) by XREAL_1: 7;

      then x0 <= (x0 + r1) by A18, XXREAL_0: 2;

      then

       A31: x0 in [.x0, (x0 + r1).] by XXREAL_1: 1;

      (x0 + r) in { g : x0 <= g & g <= (x0 + r1) } by A18, A30;

      then (x0 + r) in [.x0, (x0 + r1).] by RCOMP_1:def 1;

      then [.x0, (x0 + r).] c= [.x0, (x0 + r1).] by A31, XXREAL_2:def 12;

      then

       A32: [.x0, (x0 + r).] c= ( dom f1) by A6;

      then [.x0, (x0 + r).] c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by A29, XBOOLE_1: 19;

      then

       A33: [.x0, (x0 + r).] c= ( dom (f1 / f2)) by RFUNCT_1:def 1;

      

       A34: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f1 / f2)) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) is convergent & ( lim ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)))) = (((( Rdiff (f1,x0)) * (f2 . x0)) - (( Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2 ))

      proof

        let h, c;

        assume that

         A35: ( rng c) = {x0} and

         A36: ( rng (h + c)) c= ( dom (f1 / f2)) and

         A37: for n be Nat holds (h . n) > 0 ;

        

         A38: ( rng (h + c)) c= (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) by A36, RFUNCT_1:def 1;

         0 <= r & (x0 + 0 ) = x0 by A5, A17, XXREAL_0: 15;

        then x0 <= (x0 + r) by XREAL_1: 7;

        then

         A39: x0 in [.x0, (x0 + r).] by XXREAL_1: 1;

        then

         A40: x0 in ( dom f1) by A32;

        

         A41: ( rng c) c= ( dom f1) by A35, A40, TARSKI:def 1;

        (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) c= ( dom f1) by XBOOLE_1: 17;

        then

         A42: ( rng (h + c)) c= ( dom f1) by A38;

        then

         A43: ( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = ( Rdiff (f1,x0)) by A1, A35, A37, Th15;

        

         A44: x0 in (( dom f2) \ (f2 " { 0 })) by A29, A39;

        ( rng c) c= (( dom f2) \ (f2 " { 0 })) by A35, A44, TARSKI:def 1;

        then

         A45: ( rng c) c= ( dom (f2 ^ )) by RFUNCT_1:def 2;

        then

         A46: ( rng c) c= (( dom f1) /\ ( dom (f2 ^ ))) by A41, XBOOLE_1: 19;

        

         A47: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A35, A37, A42;

        

         A48: (f2 /* c) is non-zero by A45, RFUNCT_2: 11;

         A49:

        now

          let n;

          

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

          .= (((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* c)) . n) - (((f1 /* c) (#) (f2 /* (h + c))) . n))) by RFUNCT_2: 1

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

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

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

          .= (((((h " ) . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h " ) . n) * (((f2 /* (h + c)) . n) - ((f2 /* c) . n))))) by RFUNCT_2: 1

          .= (((((h " ) . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) - (((f1 /* c) . n) * (((h " ) . n) * (((f2 /* (h + c)) - (f2 /* c)) . n)))) by RFUNCT_2: 1

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

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

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

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

          .= (((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) . n) by RFUNCT_2: 1;

        end;

        now

          let n;

          

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

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

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

        end;

        then

         A50: ((f2 /* c) + ((f2 /* (h + c)) - (f2 /* c))) = (f2 /* (h + c)) by FUNCT_2: 63;

        (( dom f1) /\ (( dom f2) \ (f2 " { 0 }))) c= (( dom f2) \ (f2 " { 0 })) by XBOOLE_1: 17;

        then

         A51: ( rng (h + c)) c= (( dom f2) \ (f2 " { 0 })) by A38;

        then

         A52: ( rng (h + c)) c= ( dom (f2 ^ )) by RFUNCT_1:def 2;

        then

         A53: ( rng (h + c)) c= (( dom f1) /\ ( dom (f2 ^ ))) by A42, XBOOLE_1: 19;

        

         A54: (f2 /* (h + c)) is non-zero by A52, RFUNCT_2: 11;

        then

         A55: ((f2 /* (h + c)) (#) (f2 /* c)) is non-zero by A48, SEQ_1: 35;

        ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = ((h " ) (#) (((f1 (#) (f2 ^ )) /* (h + c)) - ((f1 / f2) /* c))) by RFUNCT_1: 31

        .= ((h " ) (#) (((f1 (#) (f2 ^ )) /* (h + c)) - ((f1 (#) (f2 ^ )) /* c))) by RFUNCT_1: 31

        .= ((h " ) (#) (((f1 /* (h + c)) (#) ((f2 ^ ) /* (h + c))) - ((f1 (#) (f2 ^ )) /* c))) by A53, RFUNCT_2: 8

        .= ((h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 (#) (f2 ^ )) /* c))) by A52, RFUNCT_2: 12

        .= ((h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) (#) ((f2 ^ ) /* c)))) by A46, RFUNCT_2: 8

        .= ((h " ) (#) (((f1 /* (h + c)) /" (f2 /* (h + c))) - ((f1 /* c) /" (f2 /* c)))) by A45, RFUNCT_2: 12

        .= ((h " ) (#) ((((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c)))) /" ((f2 /* (h + c)) (#) (f2 /* c)))) by A54, A48, SEQ_1: 50

        .= (((h " ) (#) (((f1 /* (h + c)) (#) (f2 /* c)) - ((f1 /* c) (#) (f2 /* (h + c))))) /" ((f2 /* (h + c)) (#) (f2 /* c))) by SEQ_1: 41;

        then

         A56: ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c))) = (((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) /" ((f2 /* (h + c)) (#) (f2 /* c))) by A49, FUNCT_2: 63;

        (( dom f2) \ (f2 " { 0 })) c= ( dom f2) by XBOOLE_1: 36;

        then

         A57: ( rng (h + c)) c= ( dom f2) by A51;

        then

         A58: ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) = ( Rdiff (f2,x0)) by A2, A35, A37, Th15;

        

         A59: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A35, A37, A57;

        now

          let n;

          

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

          

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

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

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

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

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

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

        end;

        then

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

        

         A62: for m holds (c . m) = x0

        proof

          let m;

          (c . m) in ( rng c) by VALUED_0: 28;

          hence thesis by A35, TARSKI:def 1;

        end;

        

         A63: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f1 /* c) . m) - (f1 . x0)).| < g

        proof

          let g be Real such that

           A64: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A65: m in NAT by ORDINAL1:def 12;

           |.(((f1 /* c) . m) - (f1 . x0)).| = |.((f1 . (c . m)) - (f1 . x0)).| by A41, FUNCT_2: 108, A65

          .= |.((f1 . x0) - (f1 . x0)).| by A62, A65

          .= 0 by ABSVALUE:def 1;

          hence thesis by A64;

        end;

        then

         A66: (f1 /* c) is convergent by SEQ_2:def 6;

        then

         A67: ( lim (f1 /* c)) = (f1 . x0) by A63, SEQ_2:def 7;

        ( dom (f2 ^ )) = (( dom f2) \ (f2 " { 0 })) by RFUNCT_1:def 2;

        then

         A68: ( dom (f2 ^ )) c= ( dom f2) by XBOOLE_1: 36;

        

         A69: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f2 /* c) . m) - (f2 . x0)).| < g

        proof

          let g be Real such that

           A70: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A71: m in NAT by ORDINAL1:def 12;

           |.(((f2 /* c) . m) - (f2 . x0)).| = |.((f2 . (c . m)) - (f2 . x0)).| by A45, A68, FUNCT_2: 108, XBOOLE_1: 1, A71

          .= |.((f2 . x0) - (f2 . x0)).| by A62, A71

          .= 0 by ABSVALUE:def 1;

          hence thesis by A70;

        end;

        then

         A72: (f2 /* c) is convergent by SEQ_2:def 6;

        then

         A73: ( lim (f2 /* c)) = (f2 . x0) by A69, SEQ_2:def 7;

        (h (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A59;

        then

         A74: (f2 /* (h + c)) is convergent by A72, A61, A50;

        then

         A75: ((f2 /* (h + c)) (#) (f2 /* c)) is convergent by A72;

        ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) is convergent by A2, A35, A37, A57;

        

        then ( lim (h (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) = (( lim h) * ( lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) by SEQ_2: 15

        .= 0 ;

        then 0 = (( lim (f2 /* (h + c))) - (f2 . x0)) by A72, A73, A61, A74, SEQ_2: 12;

        then

         A76: ( lim ((f2 /* (h + c)) (#) (f2 /* c))) = ((f2 . x0) ^2 ) by A72, A73, A74, SEQ_2: 15;

        

         A77: ( lim ((f2 /* (h + c)) (#) (f2 /* c))) <> 0

        proof

          assume not thesis;

          then (f2 . x0) = 0 by A76, XCMPLX_1: 6;

          hence contradiction by A8, A4, A15, A12;

        end;

        ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A1, A35, A37, A42;

        then

         A78: (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) is convergent by A72;

        

         A79: ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) is convergent by A59, A66;

        then

         A80: ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))))) is convergent by A78;

        

        then ( lim ((h " ) (#) (((f1 / f2) /* (h + c)) - ((f1 / f2) /* c)))) = (( lim ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) - ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))))) / ( lim ((f2 /* (h + c)) (#) (f2 /* c)))) by A55, A75, A77, A56, SEQ_2: 24

        .= ((( lim (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) - ( lim ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))))) / ( lim ((f2 /* (h + c)) (#) (f2 /* c)))) by A79, A78, SEQ_2: 12

        .= (((( lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) * ( lim (f2 /* c))) - ( lim ((f1 /* c) (#) ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))))) / ( lim ((f2 /* (h + c)) (#) (f2 /* c)))) by A47, A72, SEQ_2: 15

        .= (((( Rdiff (f1,x0)) * (f2 . x0)) - (( Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2 )) by A43, A59, A58, A66, A67, A73, A76, SEQ_2: 15;

        hence thesis by A55, A75, A77, A80, A56, SEQ_2: 23;

      end;

       0 < r by A5, A17, XXREAL_0: 15;

      hence thesis by A33, A34, Th15;

    end;

    theorem :: FDIFF_3:19

    f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in x0 & (f2 . x0) <> 0 implies (f1 / f2) is_right_differentiable_in x0 & ( Rdiff ((f1 / f2),x0)) = (((( Rdiff (f1,x0)) * (f2 . x0)) - (( Rdiff (f2,x0)) * (f1 . x0))) / ((f2 . x0) ^2 ))

    proof

      assume that

       A1: f1 is_right_differentiable_in x0 and

       A2: f2 is_right_differentiable_in x0 and

       A3: (f2 . x0) <> 0 ;

      consider r1 such that

       A4: r1 > 0 and [.x0, (x0 + r1).] c= ( dom f2) and

       A5: for g st g in [.x0, (x0 + r1).] holds (f2 . g) <> 0 by A2, A3, Th7, Th8;

      now

        take r1;

        thus r1 > 0 by A4;

        let g;

        assume that g in ( dom f2) and

         A6: g in [.x0, (x0 + r1).];

        thus (f2 . g) <> 0 by A5, A6;

      end;

      hence thesis by A1, A2, Lm3;

    end;

    

     Lm4: f is_right_differentiable_in x0 & (ex r0 st r0 > 0 & for g st g in ( dom f) & g in [.x0, (x0 + r0).] holds (f . g) <> 0 ) implies (f ^ ) is_right_differentiable_in x0 & ( Rdiff ((f ^ ),x0)) = ( - (( Rdiff (f,x0)) / ((f . x0) ^2 )))

    proof

      

       A1: ( 0 + x0) = x0;

      assume

       A2: f is_right_differentiable_in x0;

      then

      consider r2 such that

       A3: 0 < r2 and

       A4: [.x0, (x0 + r2).] c= ( dom f);

      given r0 such that

       A5: r0 > 0 and

       A6: for g st g in ( dom f) & g in [.x0, (x0 + r0).] holds (f . g) <> 0 ;

      set r3 = ( min (r0,r2));

       0 <= r3 by A5, A3, XXREAL_0: 15;

      then

       A7: x0 <= (x0 + r3) by A1, XREAL_1: 6;

      r3 <= r2 by XXREAL_0: 17;

      then

       A8: (x0 + r3) <= (x0 + r2) by XREAL_1: 7;

      then x0 <= (x0 + r2) by A7, XXREAL_0: 2;

      then

       A9: x0 in [.x0, (x0 + r2).] by XXREAL_1: 1;

      (x0 + r3) in { g : x0 <= g & g <= (x0 + r2) } by A7, A8;

      then (x0 + r3) in [.x0, (x0 + r2).] by RCOMP_1:def 1;

      then [.x0, (x0 + r3).] c= [.x0, (x0 + r2).] by A9, XXREAL_2:def 12;

      then

       A10: [.x0, (x0 + r3).] c= ( dom f) by A4;

      r3 <= r0 by XXREAL_0: 17;

      then

       A11: (x0 + r3) <= (x0 + r0) by XREAL_1: 7;

      then x0 <= (x0 + r0) by A7, XXREAL_0: 2;

      then

       A12: x0 in [.x0, (x0 + r0).] by XXREAL_1: 1;

      (x0 + r3) in { g : x0 <= g & g <= (x0 + r0) } by A7, A11;

      then (x0 + r3) in [.x0, (x0 + r0).] by RCOMP_1:def 1;

      then

       A13: [.x0, (x0 + r3).] c= [.x0, (x0 + r0).] by A12, XXREAL_2:def 12;

      

       A14: [.x0, (x0 + r3).] c= ( dom (f ^ ))

      proof

        assume not thesis;

        then

        consider x be object such that

         A15: x in [.x0, (x0 + r3).] and

         A16: not x in ( dom (f ^ ));

        reconsider x as Real by A15;

        

         A17: not x in (( dom f) \ (f " { 0 })) by A16, RFUNCT_1:def 2;

        now

          per cases by A17, XBOOLE_0:def 5;

            suppose not x in ( dom f);

            hence contradiction by A10, A15;

          end;

            suppose

             A18: x in (f " { 0 });

            then (f . x) in { 0 } by FUNCT_1:def 7;

            then

             A19: (f . x) = 0 by TARSKI:def 1;

            x in ( dom f) by A18, FUNCT_1:def 7;

            hence contradiction by A6, A13, A15, A19;

          end;

        end;

        hence contradiction;

      end;

      

       A20: x0 in [.x0, (x0 + r3).] by A7, XXREAL_1: 1;

      

       A21: for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom (f ^ )) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c))) is convergent & ( lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)))) = ( - (( Rdiff (f,x0)) / ((f . x0) ^2 )))

      proof

        let h, c;

        assume that

         A22: ( rng c) = {x0} and

         A23: ( rng (h + c)) c= ( dom (f ^ )) and

         A24: for n be Nat holds (h . n) > 0 ;

        

         A25: for m holds (c . m) = x0

        proof

          let m;

          (c . m) in ( rng c) by VALUED_0: 28;

          hence thesis by A22, TARSKI:def 1;

        end;

        

         A26: (( dom f) \ (f " { 0 })) c= ( dom f) by XBOOLE_1: 36;

        ( rng (h + c)) c= (( dom f) \ (f " { 0 })) by A23, RFUNCT_1:def 2;

        then

         A27: ( rng (h + c)) c= ( dom f) by A26;

        then

         A28: ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ( Rdiff (f,x0)) by A2, A22, A24, Th15;

        

         A29: ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A2, A22, A24, A27;

        then

         A30: ( - ((h " ) (#) ((f /* (h + c)) - (f /* c)))) is convergent;

        x0 in ( dom (f ^ )) by A20, A14;

        then

         A31: x0 in (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

        ( rng c) c= (( dom f) \ (f " { 0 })) by A22, A31, TARSKI:def 1;

        then

         A32: ( rng c) c= ( dom (f ^ )) by RFUNCT_1:def 2;

        then

         A33: (f /* c) is non-zero by RFUNCT_2: 11;

        now

          let n;

          

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

          

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

          .= (((h (#) (h " )) . n) * (((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

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

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

        end;

        then

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

        

         A36: (f /* (h + c)) is non-zero by A23, RFUNCT_2: 11;

        then

         A37: ((f /* (h + c)) (#) (f /* c)) is non-zero by A33, SEQ_1: 35;

        now

          let n;

          

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

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

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

        end;

        then

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

        ( dom (f ^ )) = (( dom f) \ (f " { 0 })) by RFUNCT_1:def 2;

        then

         A39: ( dom (f ^ )) c= ( dom f) by XBOOLE_1: 36;

        

         A40: for g be Real st 0 < g holds ex n be Nat st for m be Nat st n <= m holds |.(((f /* c) . m) - (f . x0)).| < g

        proof

          let g be Real such that

           A41: 0 < g;

          take n = 0 ;

          let m be Nat such that n <= m;

          

           A42: m in NAT by ORDINAL1:def 12;

           |.(((f /* c) . m) - (f . x0)).| = |.((f . (c . m)) - (f . x0)).| by A32, A39, FUNCT_2: 108, XBOOLE_1: 1, A42

          .= |.((f . x0) - (f . x0)).| by A25, A42

          .= 0 by ABSVALUE:def 1;

          hence thesis by A41;

        end;

        then

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

        then

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

        (h (#) ((h " ) (#) ((f /* (h + c)) - (f /* c)))) is convergent by A29;

        then

         A45: (f /* (h + c)) is convergent by A43, A35, A38;

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

        .= 0 ;

        then 0 = (( lim (f /* (h + c))) - (f . x0)) by A43, A44, A35, A45, SEQ_2: 12;

        then

         A46: ( lim ((f /* (h + c)) (#) (f /* c))) = ((f . x0) ^2 ) by A43, A44, A45, SEQ_2: 15;

        

         A47: ( lim ((f /* (h + c)) (#) (f /* c))) <> 0

        proof

          assume not thesis;

          then (f . x0) = 0 by A46, XCMPLX_1: 6;

          hence contradiction by A6, A4, A12, A9;

        end;

        now

          let n;

          

           A48: ((f /* (h + c)) . n) <> 0 & ((f /* c) . n) <> 0 by A36, A33, SEQ_1: 5;

          

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

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

          .= (((h " ) . n) * ((((f /* (h + c)) " ) . n) - (((f ^ ) /* c) . n))) by A23, RFUNCT_2: 12

          .= (((h " ) . n) * ((((f /* (h + c)) " ) . n) - (((f /* c) " ) . n))) by A32, RFUNCT_2: 12

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

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

          .= (((h " ) . n) * ((1 / ((f /* (h + c)) . n)) - (((f /* c) . n) " ))) by XCMPLX_1: 215

          .= (((h " ) . n) * ((1 / ((f /* (h + c)) . n)) - (1 / ((f /* c) . n)))) by XCMPLX_1: 215

          .= (((h " ) . n) * (((1 * ((f /* c) . n)) - (1 * ((f /* (h + c)) . n))) / (((f /* (h + c)) . n) * ((f /* c) . n)))) by A48, XCMPLX_1: 130

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

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

          .= (((h " ) . n) * ( - ((((f /* (h + c)) - (f /* c)) . n) / (((f /* (h + c)) (#) (f /* c)) . n)))) by XCMPLX_1: 187

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

          .= ( - ((((h " ) . n) * (((f /* (h + c)) - (f /* c)) . n)) / (((f /* (h + c)) (#) (f /* c)) . n))) by XCMPLX_1: 74

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

          .= ( - ((((h " ) (#) ((f /* (h + c)) - (f /* c))) . n) * ((((f /* (h + c)) (#) (f /* c)) . n) " ))) by XCMPLX_0:def 9

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

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

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

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

        end;

        then

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

        

         A50: ((f /* (h + c)) (#) (f /* c)) is convergent by A43, A45;

        

        then ( lim ((h " ) (#) (((f ^ ) /* (h + c)) - ((f ^ ) /* c)))) = (( lim ( - ((h " ) (#) ((f /* (h + c)) - (f /* c))))) / ((f . x0) ^2 )) by A37, A46, A47, A30, A49, SEQ_2: 24

        .= (( - ( Rdiff (f,x0))) / ((f . x0) ^2 )) by A29, A28, SEQ_2: 10

        .= ( - (( Rdiff (f,x0)) / ((f . x0) ^2 ))) by XCMPLX_1: 187;

        hence thesis by A37, A50, A47, A30, A49, SEQ_2: 23;

      end;

       0 < r3 by A5, A3, XXREAL_0: 15;

      hence thesis by A14, A21, Th15;

    end;

    theorem :: FDIFF_3:20

    f is_right_differentiable_in x0 & (f . x0) <> 0 implies (f ^ ) is_right_differentiable_in x0 & ( Rdiff ((f ^ ),x0)) = ( - (( Rdiff (f,x0)) / ((f . x0) ^2 )))

    proof

      assume that

       A1: f is_right_differentiable_in x0 and

       A2: (f . x0) <> 0 ;

      consider r1 such that

       A3: r1 > 0 and [.x0, (x0 + r1).] c= ( dom f) and

       A4: for g st g in [.x0, (x0 + r1).] holds (f . g) <> 0 by A1, A2, Th7, Th8;

      now

        take r1;

        thus r1 > 0 by A3;

        let g;

        assume that g in ( dom f) and

         A5: g in [.x0, (x0 + r1).];

        thus (f . g) <> 0 by A4, A5;

      end;

      hence thesis by A1, Lm4;

    end;

    theorem :: FDIFF_3:21

    f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & ( Rdiff (f,x0)) = ( Ldiff (f,x0)) implies f is_differentiable_in x0 & ( diff (f,x0)) = ( Rdiff (f,x0)) & ( diff (f,x0)) = ( Ldiff (f,x0))

    proof

      assume that

       A1: f is_right_differentiable_in x0 and

       A2: f is_left_differentiable_in x0 and

       A3: ( Rdiff (f,x0)) = ( Ldiff (f,x0));

      

       A4: ex N be Neighbourhood of x0 st N c= ( dom f)

      proof

        consider r2 such that

         A5: r2 > 0 and

         A6: [.x0, (x0 + r2).] c= ( dom f) by A1;

        consider r1 such that

         A7: r1 > 0 and

         A8: [.(x0 - r1), x0.] c= ( dom f) by A2;

        set r = ( min (r1,r2));

        r > 0 by A7, A5, XXREAL_0: 15;

        then

        reconsider N = ].(x0 - r), (x0 + r).[ as Neighbourhood of x0 by RCOMP_1:def 6;

        take N;

        let x be object;

        assume x in N;

        then x in { g : (x0 - r) < g & g < (x0 + r) } by RCOMP_1:def 2;

        then

        consider g such that

         A9: g = x and

         A10: (x0 - r) < g and

         A11: g < (x0 + r);

        now

          per cases ;

            suppose

             A12: g <= x0;

            r <= r1 by XXREAL_0: 17;

            then (x0 - r1) <= (x0 - r) by XREAL_1: 13;

            then (x0 - r1) <= g by A10, XXREAL_0: 2;

            then g in { g1 : (x0 - r1) <= g1 & g1 <= x0 } by A12;

            then g in [.(x0 - r1), x0.] by RCOMP_1:def 1;

            hence thesis by A8, A9;

          end;

            suppose

             A13: g > x0;

            r <= r2 by XXREAL_0: 17;

            then (x0 + r) <= (x0 + r2) by XREAL_1: 7;

            then g <= (x0 + r2) by A11, XXREAL_0: 2;

            then g in { g1 : x0 <= g1 & g1 <= (x0 + r2) } by A13;

            then g in [.x0, (x0 + r2).] by RCOMP_1:def 1;

            hence thesis by A6, A9;

          end;

        end;

        hence thesis;

      end;

      for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ( Ldiff (f,x0))

      proof

        let h, c;

        assume that

         A14: ( rng c) = {x0} and

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

        

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

        proof

          consider S be Neighbourhood of x0 such that

           A17: S c= ( dom f) by A4;

          x0 in S by RCOMP_1: 16;

          hence thesis by A14, A17, ZFMISC_1: 31;

        end;

        now

          per cases ;

            suppose ex N be Element of NAT st for n st n >= N holds (h . n) > 0 ;

            then

            consider N be Element of NAT such that

             A18: for n st n >= N holds (h . n) > 0 ;

            set h1 = (h ^\ N);

            

             A19: for n be Nat holds (h1 . n) > 0

            proof

              let n be Nat;

              (h1 . n) = (h . (n + N)) & (N + 0 ) <= (n + N) by NAT_1:def 3, XREAL_1: 7;

              hence thesis by A18;

            end;

            set c1 = (c ^\ N);

            

             A20: ( rng c1) = {x0}

            proof

              thus ( rng c1) c= {x0} by A14, VALUED_0: 21;

              let x be object;

              

               A21: (c . N) in ( rng c) by VALUED_0: 28;

              assume x in {x0};

              then

               A22: x = x0 by TARSKI:def 1;

              (c1 . 0 ) = (c . ( 0 + N)) by NAT_1:def 3

              .= (c . N);

              then (c1 . 0 ) = x by A14, A22, A21, TARSKI:def 1;

              hence thesis by VALUED_0: 28;

            end;

            

             A23: (h1 + c1) = ((h + c) ^\ N) by SEQM_3: 15;

            

            then

             A24: ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) = ((h1 " ) (#) (((f /* (h + c)) ^\ N) - (f /* c1))) by A15, VALUED_0: 27

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

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

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

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

            ( rng (h1 + c1)) c= ( rng (h + c)) by A23, VALUED_0: 21;

            then

             A25: ( rng (h1 + c1)) c= ( dom f) by A15;

            then

             A26: ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) is convergent by A1, A20, A19;

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

            ( lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1)))) = ( Rdiff (f,x0)) by A1, A20, A25, A19, Th15;

            hence ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ( Ldiff (f,x0)) by A3, A26, A24, SEQ_4: 22;

          end;

            suppose

             A27: for N be Element of NAT holds ex n st n >= N & (h . n) <= 0 ;

            now

              per cases ;

                suppose ex M be Element of NAT st for m st m >= M holds (h . m) < 0 ;

                then

                consider M be Element of NAT such that

                 A28: for n st n >= M holds (h . n) < 0 ;

                set h1 = (h ^\ M);

                

                 A29: for n be Nat holds (h1 . n) < 0

                proof

                  let n be Nat;

                  (h1 . n) = (h . (n + M)) & (M + 0 ) <= (n + M) by NAT_1:def 3, XREAL_1: 7;

                  hence thesis by A28;

                end;

                set c1 = (c ^\ M);

                

                 A30: ( rng c1) = {x0}

                proof

                  thus ( rng c1) c= {x0} by A14, VALUED_0: 21;

                  let x be object;

                  

                   A31: (c . M) in ( rng c) by VALUED_0: 28;

                  assume x in {x0};

                  then

                   A32: x = x0 by TARSKI:def 1;

                  (c1 . 0 ) = (c . ( 0 + M)) by NAT_1:def 3

                  .= (c . M);

                  then (c1 . 0 ) = x by A14, A32, A31, TARSKI:def 1;

                  hence thesis by VALUED_0: 28;

                end;

                

                 A33: (h1 + c1) = ((h + c) ^\ M) by SEQM_3: 15;

                

                then

                 A34: ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) = ((h1 " ) (#) (((f /* (h + c)) ^\ M) - (f /* c1))) by A15, VALUED_0: 27

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

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

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

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

                ( rng (h1 + c1)) c= ( rng (h + c)) by A33, VALUED_0: 21;

                then

                 A35: ( rng (h1 + c1)) c= ( dom f) by A15;

                then

                 A36: ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) is convergent by A2, A30, A29;

                hence ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent by A34, SEQ_4: 21;

                ( lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1)))) = ( Ldiff (f,x0)) by A2, A30, A35, A29, Th9;

                hence ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ( Ldiff (f,x0)) by A36, A34, SEQ_4: 22;

              end;

                suppose

                 A37: for M be Element of NAT holds ex m st m >= M & (h . m) >= 0 ;

                set s = ((h " ) (#) ((f /* (h + c)) - (f /* c)));

                defpred R[ Real] means $1 > 0 ;

                defpred P[ Real] means $1 < 0 ;

                

                 A38: for N be Element of NAT holds ex n st n >= N & P[(h . n)]

                proof

                  let m;

                  consider n such that

                   A39: n >= m and

                   A40: (h . n) <= 0 by A27;

                  take n;

                  thus n >= m by A39;

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

                  hence thesis by A40;

                end;

                consider q1 be increasing sequence of NAT such that

                 A41: (for n be Nat holds P[((h * q1) . n)]) & for n st (for r st r = (h . n) holds P[r]) holds ex m st n = (q1 . m) from FDIFF_2:sch 1( A38);

                

                 A42: for N be Element of NAT holds ex n st n >= N & R[(h . n)]

                proof

                  let m;

                  consider n such that

                   A43: n >= m and

                   A44: (h . n) >= 0 by A37;

                  take n;

                  thus n >= m by A43;

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

                  hence thesis by A44;

                end;

                consider q2 be increasing sequence of NAT such that

                 A45: (for n be Nat holds R[((h * q2) . n)]) & for n st (for r st r = (h . n) holds R[r]) holds ex m st n = (q2 . m) from FDIFF_2:sch 1( A42);

                set h1 = (h * q1);

                reconsider h1 as subsequence of h;

                

                 A46: h1 is convergent by SEQ_4: 16;

                

                 A47: ( lim h) = 0 ;

                then

                 A48: ( lim h1) = 0 by SEQ_4: 17;

                set h2 = (h * q2);

                

                 A49: h2 is convergent by SEQ_4: 16;

                ( lim h2) = 0 by A47, SEQ_4: 17;

                then

                reconsider h2 as 0 -convergent non-zero Real_Sequence by A49, FDIFF_1:def 1;

                set c2 = (c * q2);

                

                 A50: ( rng c2) = {x0} by A14, VALUED_0: 26;

                reconsider c2 as constant Real_Sequence;

                ( rng ((h + c) * q2)) c= ( rng (h + c)) by VALUED_0: 21;

                then ( rng ((h + c) * q2)) c= ( dom f) by A15;

                then ( rng (h2 + c2)) c= ( dom f) by RFUNCT_2: 2;

                then

                 A51: ((h2 " ) (#) ((f /* (h2 + c2)) - (f /* c2))) is convergent & ( lim ((h2 " ) (#) ((f /* (h2 + c2)) - (f /* c2)))) = ( Ldiff (f,x0)) by A1, A3, A45, A50, Th15;

                

                 A52: ((h2 " ) (#) ((f /* (h2 + c2)) - (f /* c2))) = ((h2 " ) (#) ((f /* ((h + c) * q2)) - (f /* c2))) by RFUNCT_2: 2

                .= ((h2 " ) (#) (((f /* (h + c)) * q2) - (f /* c2))) by A15, FUNCT_2: 110

                .= (((h " ) * q2) (#) (((f /* (h + c)) * q2) - (f /* c2))) by RFUNCT_2: 5

                .= (((h " ) * q2) (#) (((f /* (h + c)) * q2) - ((f /* c) * q2))) by A16, FUNCT_2: 110

                .= (((h " ) * q2) (#) (((f /* (h + c)) - (f /* c)) * q2)) by RFUNCT_2: 2

                .= (((h " ) (#) ((f /* (h + c)) - (f /* c))) * q2) by RFUNCT_2: 2;

                reconsider h1 as 0 -convergent non-zero Real_Sequence by A46, A48, FDIFF_1:def 1;

                set c1 = (c * q1);

                

                 A53: ( rng c1) = {x0} by A14, VALUED_0: 26;

                reconsider c1 as constant Real_Sequence;

                ( rng ((h + c) * q1)) c= ( rng (h + c)) by VALUED_0: 21;

                then ( rng ((h + c) * q1)) c= ( dom f) by A15;

                then ( rng (h1 + c1)) c= ( dom f) by RFUNCT_2: 2;

                then

                 A54: ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) is convergent & ( lim ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1)))) = ( Ldiff (f,x0)) by A2, A41, A53, Th9;

                

                 A55: ((h1 " ) (#) ((f /* (h1 + c1)) - (f /* c1))) = ((h1 " ) (#) ((f /* ((h + c) * q1)) - (f /* c1))) by RFUNCT_2: 2

                .= ((h1 " ) (#) (((f /* (h + c)) * q1) - (f /* c1))) by A15, FUNCT_2: 110

                .= (((h " ) * q1) (#) (((f /* (h + c)) * q1) - (f /* c1))) by RFUNCT_2: 5

                .= (((h " ) * q1) (#) (((f /* (h + c)) * q1) - ((f /* c) * q1))) by A16, FUNCT_2: 110

                .= (((h " ) * q1) (#) (((f /* (h + c)) - (f /* c)) * q1)) by RFUNCT_2: 2

                .= (((h " ) (#) ((f /* (h + c)) - (f /* c))) * q1) by RFUNCT_2: 2;

                

                 A56: for g1 be Real st 0 < g1 holds ex n be Nat st for m be Nat st n <= m holds |.((s . m) - ( Ldiff (f,x0))).| < g1

                proof

                  let g1 be Real;

                  assume

                   A57: 0 < g1;

                  then

                  consider n1 be Nat such that

                   A58: for m be Nat st n1 <= m holds |.(((s * q1) . m) - ( Ldiff (f,x0))).| < g1 by A54, A55, SEQ_2:def 7;

                  consider n2 be Nat such that

                   A59: for m be Nat st n2 <= m holds |.(((s * q2) . m) - ( Ldiff (f,x0))).| < g1 by A51, A52, A57, SEQ_2:def 7;

                  take n = ( max ((q1 . n1),(q2 . n2)));

                  let m be Nat such that

                   A60: n <= m;

                  

                   A61: m in NAT by ORDINAL1:def 12;

                  

                   A62: n >= (q2 . n2) by XXREAL_0: 25;

                  

                   A63: n >= (q1 . n1) by XXREAL_0: 25;

                  per cases ;

                    suppose (h . m) > 0 ;

                    then for r st r = (h . m) holds r > 0 ;

                    then

                    consider k such that

                     A64: m = (q2 . k) by A45, A61;

                    

                     A65: n2 in NAT by ORDINAL1:def 12;

                    ( dom q2) = NAT & (q2 . k) >= (q2 . n2) by A60, A62, A64, FUNCT_2:def 1, XXREAL_0: 2;

                    then not k < n2 by VALUED_0:def 13, A65;

                    then |.(((s * q2) . k) - ( Ldiff (f,x0))).| < g1 by A59;

                    hence thesis by A64, FUNCT_2: 15;

                  end;

                    suppose

                     A66: (h . m) <= 0 ;

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

                    then for r st r = (h . m) holds r < 0 by A66;

                    then

                    consider k such that

                     A67: m = (q1 . k) by A41, A61;

                    

                     A68: n1 in NAT by ORDINAL1:def 12;

                    ( dom q1) = NAT & (q1 . k) >= (q1 . n1) by A60, A63, A67, FUNCT_2:def 1, XXREAL_0: 2;

                    then not k < n1 by VALUED_0:def 13, A68;

                    then |.(((s * q1) . k) - ( Ldiff (f,x0))).| < g1 by A58;

                    hence thesis by A67, FUNCT_2: 15;

                  end;

                end;

                hence s is convergent by SEQ_2:def 6;

                hence ( lim s) = ( Ldiff (f,x0)) by A56, SEQ_2:def 7;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      hence thesis by A3, A4, FDIFF_2: 12;

    end;

    theorem :: FDIFF_3:22

    f is_differentiable_in x0 implies f is_right_differentiable_in x0 & f is_left_differentiable_in x0 & ( diff (f,x0)) = ( Rdiff (f,x0)) & ( diff (f,x0)) = ( Ldiff (f,x0))

    proof

      assume

       A1: f is_differentiable_in x0;

      then

      consider N be Neighbourhood of x0 such that

       A2: N c= ( dom f) by FDIFF_2: 11;

      consider g1 be Real such that

       A3: g1 > 0 and

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

      

       A5: g1 > (g1 / 2) by A3, XREAL_1: 216;

      

       A6: ex r st r > 0 & [.x0, (x0 + r).] c= ( dom f)

      proof

        take r = (g1 / 2);

        thus r > 0 by A3, XREAL_1: 215;

         |.((x0 + (g1 / 2)) - x0).| = (g1 / 2) by A3, ABSVALUE:def 1;

        then

         A7: (x0 + r) in ].(x0 - g1), (x0 + g1).[ by A5, RCOMP_1: 1;

        x0 in ].(x0 - g1), (x0 + g1).[ by A4, RCOMP_1: 16;

        then [.x0, (x0 + r).] c= ].(x0 - g1), (x0 + g1).[ by A7, XXREAL_2:def 12;

        hence thesis by A2, A4;

      end;

      

       A8: ex r st 0 < r & [.(x0 - r), x0.] c= ( dom f)

      proof

        take r = (g1 / 2);

        thus r > 0 by A3, XREAL_1: 215;

         |.((x0 - (g1 / 2)) - x0).| = |.(( - (g1 / 2)) + 0 ).|

        .= |.(g1 / 2).| by COMPLEX1: 52

        .= (g1 / 2) by A3, ABSVALUE:def 1;

        then

         A9: (x0 - r) in ].(x0 - g1), (x0 + g1).[ by A5, RCOMP_1: 1;

        x0 in ].(x0 - g1), (x0 + g1).[ by A4, RCOMP_1: 16;

        then [.(x0 - r), x0.] c= ].(x0 - g1), (x0 + g1).[ by A9, XXREAL_2:def 12;

        hence thesis by A2, A4;

      end;

      ( diff (f,x0)) = ( diff (f,x0));

      then (for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) > 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ( diff (f,x0))) & for h, c st ( rng c) = {x0} & ( rng (h + c)) c= ( dom f) & (for n be Nat holds (h . n) < 0 ) holds ((h " ) (#) ((f /* (h + c)) - (f /* c))) is convergent & ( lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))) = ( diff (f,x0)) by A1, FDIFF_2: 12;

      hence thesis by A6, A8, Th9, Th15;

    end;