let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_left_differentiable_in x0 & f2 is_differentiable_in f1 . x0 implies ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) )
assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_differentiable_in f1 . x0 ; :: thesis: ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
consider r being Real such that
A3: ( r > 0 & [.(x0 - r),x0.] c= dom (f2 * f1) ) by A1, A2, Lm21;
A4: f1 is_Lcontinuous_in x0 by A1, FDIFF_3:5;
x0 - r < x0 by A3, XREAL_1:44;
then A5: x0 in dom (f2 * f1) by A3, XXREAL_1:1;
then A6: f1 . x0 in dom f2 by FUNCT_1:11;
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f2 * f1) & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f2 * f1) & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f2 * f1) & ( for n being Nat holds h . n < 0 ) implies ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) )
assume that
A7: rng c = {x0} and
A8: rng (h + c) c= dom (f2 * f1) and
A9: for n being Nat holds h . n < 0 ; :: thesis: ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
A10: for n being Nat holds c . n = x0

proof

let n be Nat; :: thesis: c . n = x0
c . n in rng c by VALUED_0:28;
hence c . n = x0 by A7, TARSKI:def 1; :: thesis: verum

end;

A11: now :: thesis: for x being Real st x in rng (h + c) holds
x in (left_open_halfline x0) /\ (dom f1)

let x be Real; :: thesis: ( x in rng (h + c) implies x in (left_open_halfline x0) /\ (dom f1) )
assume A12: x in rng (h + c) ; :: thesis: x in (left_open_halfline x0) /\ (dom f1)
then consider n being Element of NAT such that
A13: x = (h + c) . n by FUNCT_2:113;
x = (h . n) + (c . n) by A13, SEQ_1:7;
then x = (h . n) + x0 by A10;
then x < x0 by A9, XREAL_1:30;
then x in ].-infty,x0.[ by XXREAL_1:233;
then A14: x in left_open_halfline x0 by PROB_1:def 10;
x in dom f1 by A12, A8, FUNCT_1:11;
hence x in (left_open_halfline x0) /\ (dom f1) by A14, XBOOLE_0:def 4; :: thesis: verum

end;

then A15: rng (h + c) c= (left_open_halfline x0) /\ (dom f1) ;
then A16: rng (h + c) c= dom f1 by XBOOLE_1:18;
A17: rng c c= dom f1 by A7, A4, FDIFF_3:def 1, ZFMISC_1:31;
set a = f1 /* c;
set d = (f1 /* (h + c)) - (f1 /* c);
A18: lim h = 0 ;
lim c = c . 0 by SEQ_4:25;
then lim c = x0 by A10;
then A19: lim (h + c) = 0 + x0 by A18, SEQ_2:6
.= x0 ;
A20: f1 is_Lcontinuous_in x0 by A1, FDIFF_3:5;
then A21: f1 /* (h + c) is convergent by A15, A19, FDIFF_3:def 1;
A22: f1 . x0 = lim (f1 /* (h + c)) by A15, A19, A20, FDIFF_3:def 1;
A23: rng (f1 /* (h + c)) c= dom f2 by A8, FDIFF_2:9;

now :: thesis: for x being Real st x in rng (f1 /* c) holds
x in {(f1 . x0)}

let x be Real; :: thesis: ( x in rng (f1 /* c) implies x in {(f1 . x0)} )
assume x in rng (f1 /* c) ; :: thesis: x in {(f1 . x0)}
then consider n being Element of NAT such that
A24: (f1 /* c) . n = x by FUNCT_2:113;
c . n = x0 by A10;
then x = f1 . x0 by A17, A24, FUNCT_2:108;
hence x in {(f1 . x0)} by TARSKI:def 1; :: thesis: verum

end;

then A25: rng (f1 /* c) c= {(f1 . x0)} ;

now :: thesis: for x being Real st x in {(f1 . x0)} holds
x in rng (f1 /* c)

let x be Real; :: thesis: ( x in {(f1 . x0)} implies x in rng (f1 /* c) )
A26: (f1 /* c) . 0 in rng (f1 /* c) by VALUED_0:28;
assume x in {(f1 . x0)} ; :: thesis: x in rng (f1 /* c)
then A27: x = f1 . x0 by TARSKI:def 1;
c . 0 = x0 by A10;
hence x in rng (f1 /* c) by A17, A27, A26, FUNCT_2:108; :: thesis: verum

end;

then {(f1 . x0)} c= rng (f1 /* c) ;
then A28: rng (f1 /* c) = {(f1 . x0)} by A25, XBOOLE_0:def 10;

A29: now :: thesis: for n being Nat holds (f1 /* c) . n = (f1 /* c) . (n + 1)

let n be Nat; :: thesis: (f1 /* c) . n = (f1 /* c) . (n + 1)
(f1 /* c) . n in rng (f1 /* c) by VALUED_0:28;
then A30: (f1 /* c) . n = f1 . x0 by A25, TARSKI:def 1;
(f1 /* c) . (n + 1) in rng (f1 /* c) by VALUED_0:28;
hence (f1 /* c) . n = (f1 /* c) . (n + 1) by A25, A30, TARSKI:def 1; :: thesis: verum

end;

then A31: f1 /* c is constant by VALUED_0:25;
reconsider a = f1 /* c as constant Real_Sequence by A29, VALUED_0:25;
a . 0 in rng a by VALUED_0:28;
then a . 0 = f1 . x0 by A25, TARSKI:def 1;
then lim a = f1 . x0 by SEQ_4:25;
then A32: lim ((f1 /* (h + c)) - (f1 /* c)) = (f1 . x0) - (f1 . x0) by A21, A22, SEQ_2:12
.= 0 ;
( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

proof

per cases ( ex k being Element of NAT st
for n being Element of NAT st k <= n holds
(f1 /* (h + c)) . n <> f1 . x0 or for k being Element of NAT ex n being Element of NAT st
( k <= n & (f1 /* (h + c)) . n = f1 . x0 ) ) ;

suppose ex k being Element of NAT st
for n being Element of NAT st k <= n holds
(f1 /* (h + c)) . n <> f1 . x0 ; :: thesis: ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

then consider k being Element of NAT such that
A33: for n being Element of NAT st k <= n holds
(f1 /* (h + c)) . n <> f1 . x0 ;

A34: now :: thesis: for n being Nat holds not (((f1 /* (h + c)) - (f1 /* c)) ^\ k) . n = 0

given n being Nat such that A35: (((f1 /* (h + c)) - (f1 /* c)) ^\ k) . n = 0 ; :: thesis: contradiction
0 = ((f1 /* (h + c)) - (f1 /* c)) . (n + k) by A35, NAT_1:def 3
.= ((f1 /* (h + c)) . (n + k)) - ((f1 /* c) . (n + k)) by RFUNCT_2:1
.= ((f1 /* (h + c)) . (n + k)) - (f1 . (c . (n + k))) by A17, FUNCT_2:108
.= ((f1 /* (h + c)) . (n + k)) - (f1 . x0) by A10 ;
hence contradiction by A33, NAT_1:12; :: thesis: verum

end;

set c1 = c ^\ k;
set h1 = h ^\ k;
set a1 = a ^\ k;
set s = ((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)));

A36: now :: thesis: for n being Element of NAT holds (((f1 /* (h + c)) - (f1 /* c)) + a) . n = (f1 /* (h + c)) . n

let n be Element of NAT ; :: thesis: (((f1 /* (h + c)) - (f1 /* c)) + a) . n = (f1 /* (h + c)) . n
thus (((f1 /* (h + c)) - (f1 /* c)) + a) . n = (((f1 /* (h + c)) - (f1 /* c)) . n) + (a . n) by SEQ_1:7
.= (((f1 /* (h + c)) . n) - (a . n)) + (a . n) by RFUNCT_2:1
.= (f1 /* (h + c)) . n ; :: thesis: verum

end;

lim (((f1 /* (h + c)) - (f1 /* c)) ^\ k) = 0 by A31, A21, A32, SEQ_4:20;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) ^\ k as non-zero 0 -convergent Real_Sequence by A31, A21, A34, SEQ_1:5, FDIFF_1:def 1;
set t = (d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)));
d1 + (a ^\ k) = (((f1 /* (h + c)) - (f1 /* c)) + a) ^\ k by SEQM_3:15;
then A37: d1 + (a ^\ k) = (f1 /* (h + c)) ^\ k by A36, FUNCT_2:63;
rng ((f1 /* (h + c)) ^\ k) c= rng (f1 /* (h + c)) by VALUED_0:21;
then A38: rng (d1 + (a ^\ k)) c= dom f2 by A23, A37;
A39: rng (a ^\ k) = {(f1 . x0)} by A28, VALUED_0:26;
then A40: lim ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) = diff (f2,(f1 . x0)) by A2, A38, FDIFF_2:12;
diff (f2,(f1 . x0)) = diff (f2,(f1 . x0)) ;
then A41: (d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) is convergent by A2, A39, A38, FDIFF_2:12;
rng ((h + c) ^\ k) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) ^\ k) c= (left_open_halfline x0) /\ (dom f1) by A11;
then A42: rng ((h ^\ k) + (c ^\ k)) c= (left_open_halfline x0) /\ (dom f1) by SEQM_3:15;
(left_open_halfline x0) /\ (dom f1) c= dom f1 by XBOOLE_1:17;
then A43: rng ((h ^\ k) + (c ^\ k)) c= dom f1 by A42;
A44: rng (c ^\ k) = {x0} by A7, VALUED_0:26;
A45: for n being Nat holds (h ^\ k) . n < 0

proof

let n be Nat; :: thesis: (h ^\ k) . n < 0
(h ^\ k) . n = h . (k + n) by NAT_1:def 3;
hence (h ^\ k) . n < 0 by A9; :: thesis: verum

end;

Ldiff (f1,x0) = Ldiff (f1,x0) ;
then A46: ((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k))) is convergent by A1, A44, A45, A43, FDIFF_3:9;
A47: ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) (#) (((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)))) = ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) (#) (((f1 /* ((h + c) ^\ k)) - (f1 /* (c ^\ k))) (#) ((h ^\ k) ")) by SEQM_3:15
.= ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) (#) ((((f1 /* (h + c)) ^\ k) - (f1 /* (c ^\ k))) (#) ((h ^\ k) ")) by A15, XBOOLE_1:18, VALUED_0:27
.= ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) (#) ((((f1 /* (h + c)) ^\ k) - ((f1 /* c) ^\ k)) (#) ((h ^\ k) ")) by A17, VALUED_0:27
.= (((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) /" d1) (#) ((((f1 /* (h + c)) ^\ k) - ((f1 /* c) ^\ k)) (#) ((h ^\ k) ")) by VALUED_1:def 10
.= (((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) /" d1) (#) (d1 (#) ((h ^\ k) ")) by SEQM_3:17
.= ((((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) /" d1) (#) d1) (#) ((h ^\ k) ") by SEQ_1:14
.= ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) (#) ((h ^\ k) ") by SEQ_1:37
.= (((f2 /* (f1 /* (h + c))) ^\ k) - (f2 /* (a ^\ k))) (#) ((h ^\ k) ") by A23, A37, VALUED_0:27
.= ((((f2 * f1) /* (h + c)) ^\ k) - (f2 /* (a ^\ k))) (#) ((h ^\ k) ") by A8, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) ^\ k) - ((f2 /* a) ^\ k)) (#) ((h ^\ k) ") by A6, A28, ZFMISC_1:31, VALUED_0:27
.= ((((f2 * f1) /* (h + c)) ^\ k) - (((f2 * f1) /* c) ^\ k)) (#) ((h ^\ k) ") by A7, A5, ZFMISC_1:31, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) ^\ k) (#) ((h ^\ k) ") by SEQM_3:17
.= ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) ^\ k) (#) ((h ") ^\ k) by SEQM_3:18
.= ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k by SEQM_3:19 ;
hence (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent by A46, A41, SEQ_4:21; :: thesis: lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0))
lim (((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)))) = Ldiff (f1,x0) by A1, A44, A45, A43, FDIFF_3:9;
then lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A47, A46, A41, A40, SEQ_2:15;
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A47, A46, A41, SEQ_4:22; :: thesis: verum

end;

suppose A48: for k being Element of NAT ex n being Element of NAT st
( k <= n & (f1 /* (h + c)) . n = f1 . x0 ) ; :: thesis: ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

defpred S₁[ object ] means $1 = f1 . x0;
A49: for k being Element of NAT ex n being Element of NAT st
( k <= n & S₁[(f1 /* (h + c)) . n] ) by A48;
consider I1 being increasing sequence of NAT such that
A50: for n being Nat holds S₁[((f1 /* (h + c)) * I1) . n] and
for n being Element of NAT st ( for r being Real st r = (f1 /* (h + c)) . n holds
S₁[r] ) holds
ex m being Element of NAT st n = I1 . m from FDIFF_2:sch 1(A49);
reconsider h1 = h * I1 as non-zero 0 -convergent Real_Sequence by FDIFF_2:6;
set c1 = c * I1;
A51: c * I1 = c by VALUED_0:26;
A52: rng (c * I1) = {x0} by A7, VALUED_0:26;
A53: rng h1 c= rng h by VALUED_0:21;
A54: for n being Nat holds h1 . n < 0

proof

let n be Nat; :: thesis: h1 . n < 0
dom h1 = NAT by FUNCT_2:def 1;
then n in dom h1 by ORDINAL1:def 12;
then h1 . n in rng h by A53, FUNCT_1:3;
then ex m being Element of NAT st h1 . n = h . m by FUNCT_2:113;
hence h1 . n < 0 by A9; :: thesis: verum

end;

reconsider c1 = c * I1 as constant Real_Sequence ;

A55: now :: thesis: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
|.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g )
assume A56: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g
reconsider n = 0 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g
let m be Nat; :: thesis: ( n <= m implies |.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g )
assume n <= m ; :: thesis: |.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g
A57: m in NAT by ORDINAL1:def 12;
|.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| = |.(((h1 ") . m) * (((f1 /* (h1 + c1)) - (f1 /* c1)) . m)).| by SEQ_1:8
.= |.(((h1 ") . m) * (((f1 /* (h1 + c1)) . m) - ((f1 /* c1) . m))).| by RFUNCT_2:1
.= |.(((h1 ") . m) * (((f1 /* (h1 + c1)) . m) - (f1 . (c . m)))).| by A17, A51, A57, FUNCT_2:108
.= |.(((h1 ") . m) * (((f1 /* (h1 + c1)) . m) - (f1 . x0))).| by A10
.= |.(((h1 ") . m) * (((f1 /* ((h + c) * I1)) . m) - (f1 . x0))).| by RFUNCT_2:2
.= |.(((h1 ") . m) * ((((f1 /* (h + c)) * I1) . m) - (f1 . x0))).| by A15, XBOOLE_1:18, FUNCT_2:110
.= |.(((h1 ") . m) * ((f1 . x0) - (f1 . x0))).| by A50
.= 0 by ABSVALUE:2 ;
hence |.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g by A56; :: thesis: verum

end;

rng ((h + c) * I1) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) * I1) c= dom f1 by A16;
then A58: rng (h1 + c1) c= dom f1 by RFUNCT_2:2;
then A59: lim ((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) = Ldiff (f1,x0) by A1, A52, A54, FDIFF_3:9;
Ldiff (f1,x0) = Ldiff (f1,x0) ;
then (h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1)) is convergent by A1, A52, A58, A54, FDIFF_3:9;
then A60: Ldiff (f1,x0) = 0 by A59, A55, SEQ_2:def 7;

now :: thesis: ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

per cases ( ex k being Element of NAT st
for n being Element of NAT st k <= n holds
(f1 /* (h + c)) . n = f1 . x0 or for k being Element of NAT ex n being Element of NAT st
( k <= n & (f1 /* (h + c)) . n <> f1 . x0 ) ) ;

suppose ex k being Element of NAT st
for n being Element of NAT st k <= n holds
(f1 /* (h + c)) . n = f1 . x0 ; :: thesis: ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

then consider k being Element of NAT such that
A61: for n being Element of NAT st k <= n holds
(f1 /* (h + c)) . n = f1 . x0 ;

A62: now :: thesis: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g )
assume A63: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
reconsider n = k as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g )
A64: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
then A65: (f1 /* (h + c)) . m = f1 . x0 by A61, A64;
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| = |.(((h ") . m) * ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) . m)).| by A60, SEQ_1:8
.= |.(((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (((f2 * f1) /* c) . m))).| by RFUNCT_2:1
.= |.(((h ") . m) * (((f2 /* (f1 /* (h + c))) . m) - (((f2 * f1) /* c) . m))).| by A8, VALUED_0:31
.= |.(((h ") . m) * ((f2 . ((f1 /* (h + c)) . m)) - (((f2 * f1) /* c) . m))).| by A23, FUNCT_2:108, A64
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - ((f2 /* (f1 /* c)) . m))).| by A7, A5, ZFMISC_1:31, A65, VALUED_0:31
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - (f2 . ((f1 /* c) . m)))).| by A6, A28, ZFMISC_1:31, FUNCT_2:108, A64
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . (c . m))))).| by A17, FUNCT_2:108, A64
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))).| by A10
.= 0 by ABSVALUE:2 ;
hence |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A63; :: thesis: verum

end;

hence (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0))
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A62, SEQ_2:def 7; :: thesis: verum

end;

suppose A66: for k being Element of NAT ex n being Element of NAT st
( k <= n & (f1 /* (h + c)) . n <> f1 . x0 ) ; :: thesis: ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

defpred S₂[ object ] means $1 <> f1 . x0;
A67: for k being Element of NAT ex n being Element of NAT st
( k <= n & S₂[(f1 /* (h + c)) . n] ) by A66;
consider I2 being increasing sequence of NAT such that
A68: for n being Nat holds S₂[((f1 /* (h + c)) * I2) . n] and
A69: for n being Element of NAT st ( for r being Real st r = (f1 /* (h + c)) . n holds
S₂[r] ) holds
ex m being Element of NAT st n = I2 . m from FDIFF_2:sch 1(A67);

A70: now :: thesis: for n being Nat holds not (((f1 /* (h + c)) - (f1 /* c)) * I2) . n = 0

given n being Nat such that A71: (((f1 /* (h + c)) - (f1 /* c)) * I2) . n = 0 ; :: thesis: contradiction
0 = ((f1 /* (h + c)) - (f1 /* c)) . (I2 . n) by A71, ORDINAL1:def 12, FUNCT_2:15
.= ((f1 /* (h + c)) . (I2 . n)) - ((f1 /* c) . (I2 . n)) by RFUNCT_2:1
.= ((f1 /* (h + c)) . (I2 . n)) - (f1 . (c . (I2 . n))) by A17, FUNCT_2:108
.= ((f1 /* (h + c)) . (I2 . n)) - (f1 . x0) by A10
.= (((f1 /* (h + c)) * I2) . n) - (f1 . x0) by FUNCT_2:15, ORDINAL1:def 12 ;
hence contradiction by A68; :: thesis: verum

end;

reconsider h2 = h * I2 as non-zero 0 -convergent Real_Sequence by FDIFF_2:6;
reconsider a1 = a * I2 as constant Real_Sequence ;
reconsider c2 = c * I2 as constant Real_Sequence ;
set s = (h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2));
lim (((f1 /* (h + c)) - (f1 /* c)) * I2) = 0 by A31, A21, A32, SEQ_4:17;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) * I2 as non-zero 0 -convergent Real_Sequence by A31, A21, SEQ_4:16, A70, SEQ_1:5, FDIFF_1:def 1;
set t = (d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1));
A72: rng a1 = {(f1 . x0)} by A28, VALUED_0:26;

A73: now :: thesis: for n being Element of NAT holds (((f1 /* (h + c)) - (f1 /* c)) + a) . n = (f1 /* (h + c)) . n

let n be Element of NAT ; :: thesis: (((f1 /* (h + c)) - (f1 /* c)) + a) . n = (f1 /* (h + c)) . n
thus (((f1 /* (h + c)) - (f1 /* c)) + a) . n = (((f1 /* (h + c)) - (f1 /* c)) . n) + (a . n) by SEQ_1:7
.= (((f1 /* (h + c)) . n) - (a . n)) + (a . n) by RFUNCT_2:1
.= (f1 /* (h + c)) . n ; :: thesis: verum

end;

d1 + a1 = (((f1 /* (h + c)) - (f1 /* c)) + a) * I2 by RFUNCT_2:2;
then A74: d1 + a1 = (f1 /* (h + c)) * I2 by A73, FUNCT_2:63;
A75: ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) (#) ((h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2))) = ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) (#) (((f1 /* ((h + c) * I2)) - (f1 /* c2)) (#) (h2 ")) by RFUNCT_2:2
.= ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) (#) ((((f1 /* (h + c)) * I2) - (f1 /* c2)) (#) (h2 ")) by A15, XBOOLE_1:18, FUNCT_2:110
.= ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) (#) ((((f1 /* (h + c)) * I2) - ((f1 /* c) * I2)) (#) (h2 ")) by A17, FUNCT_2:110
.= (((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) ((((f1 /* (h + c)) * I2) - ((f1 /* c) * I2)) (#) (h2 ")) by VALUED_1:def 10
.= (((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) (d1 (#) (h2 ")) by RFUNCT_2:2
.= ((((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) d1) (#) (h2 ") by SEQ_1:14
.= ((f2 /* (d1 + a1)) - (f2 /* a1)) (#) (h2 ") by SEQ_1:37
.= (((f2 /* (f1 /* (h + c))) * I2) - (f2 /* a1)) (#) (h2 ") by A23, A74, FUNCT_2:110
.= ((((f2 * f1) /* (h + c)) * I2) - (f2 /* a1)) (#) (h2 ") by A8, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) * I2) - ((f2 /* a) * I2)) (#) (h2 ") by A6, A28, ZFMISC_1:31, FUNCT_2:110
.= ((((f2 * f1) /* (h + c)) * I2) - (((f2 * f1) /* c) * I2)) (#) (h2 ") by A7, A5, ZFMISC_1:31, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) * I2) (#) (h2 ") by RFUNCT_2:2
.= ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) * I2) (#) ((h ") * I2) by RFUNCT_2:5
.= ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2 by RFUNCT_2:2 ;
rng ((f1 /* (h + c)) * I2) c= rng (f1 /* (h + c)) by VALUED_0:21;
then A76: rng (d1 + a1) c= dom f2 by A23, A74;
rng ((h + c) * I2) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) * I2) c= dom f1 by A16;
then A77: rng (h2 + c2) c= dom f1 by RFUNCT_2:2;
A78: rng h2 c= rng h by VALUED_0:21;
A79: for n being Nat holds h2 . n < 0

proof

let n be Nat; :: thesis: h2 . n < 0
dom h2 = NAT by FUNCT_2:def 1;
then h2 . n in rng h2 by FUNCT_1:3, ORDINAL1:def 12;
then ex m being Element of NAT st h2 . n = h . m by A78, FUNCT_2:113;
hence h2 . n < 0 by A9; :: thesis: verum

end;

A80: rng c2 = {x0} by A7, VALUED_0:26;
then A81: lim ((h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2))) = Ldiff (f1,x0) by A1, A77, A79, FDIFF_3:9;
Ldiff (f1,x0) = Ldiff (f1,x0) ;
then A82: (h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2)) is convergent by A1, A80, A77, A79, FDIFF_3:9;
diff (f2,(f1 . x0)) = diff (f2,(f1 . x0)) ;
then A83: (d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1)) is convergent by A2, A72, A76, FDIFF_2:12;
lim ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) = diff (f2,(f1 . x0)) by A2, A72, A76, FDIFF_2:12;
then A84: lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A75, A82, A81, A83, SEQ_2:15;

A85: now :: thesis: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g

set DF = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0));
let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g )
assume A86: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
consider k being Nat such that
A87: for m being Nat st k <= m holds
|.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A75, A82, A83, A84, A86, SEQ_2:def 7;
A88: k in NAT by ORDINAL1:def 12;
reconsider n = I2 . k as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g )
assume A89: n <= m ; :: thesis: |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
A90: m in NAT by ORDINAL1:def 12;

now :: thesis: |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g

per cases ( (f1 /* (h + c)) . m = f1 . x0 or (f1 /* (h + c)) . m <> f1 . x0 ) ;

suppose A91: (f1 /* (h + c)) . m = f1 . x0 ; :: thesis: |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g

|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| = |.(((h ") . m) * ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) . m)).| by A60, SEQ_1:8
.= |.(((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (((f2 * f1) /* c) . m))).| by RFUNCT_2:1
.= |.(((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - ((f2 /* (f1 /* c)) . m))).| by A7, A5, ZFMISC_1:31, VALUED_0:31
.= |.(((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . ((f1 /* c) . m)))).| by A6, A28, ZFMISC_1:31, FUNCT_2:108, A90
.= |.(((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . (f1 . (c . m))))).| by A17, FUNCT_2:108, A90
.= |.(((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . (f1 . x0)))).| by A10
.= |.(((h ") . m) * (((f2 /* (f1 /* (h + c))) . m) - (f2 . (f1 . x0)))).| by A8, VALUED_0:31
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))).| by A23, A91, FUNCT_2:108, A90
.= 0 by ABSVALUE:2 ;
hence |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A86; :: thesis: verum

end;

suppose (f1 /* (h + c)) . m <> f1 . x0 ; :: thesis: |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g

then for r1 being Real st (f1 /* (h + c)) . m = r1 holds
r1 <> f1 . x0 ;
then consider l being Element of NAT such that
A92: m = I2 . l by A69, A90;
dom I2 = NAT by FUNCT_2:def 1;
then l >= k by A89, A92, VALUED_0:def 13, A88;
then |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) . l) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A87;
hence |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A92, FUNCT_2:15; :: thesis: verum

end;

end;

end;

hence |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g ; :: thesis: verum

end;

hence (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent by SEQ_2:def 6; :: thesis: lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0))
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A85, SEQ_2:def 7; :: thesis: verum

end;

end;

end;

hence ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) ; :: thesis: verum

end;

end;

end;

hence ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) ; :: thesis: verum

end;

hence ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) by A3, FDIFF_3:9; :: thesis: verum