let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ( for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) ) holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_left_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ( for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) ) implies ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) )
assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_right_differentiable_in f1 . x0 and
A3: for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) ; :: thesis: ( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
consider r1 being Real such that
A4: ( r1 > 0 & [.(f1 . x0),((f1 . x0) + r1).] c= dom f2 ) by A2, FDIFF_3:def 3;
consider r0 being Real such that
A5: ( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) by A3, A4;
set r = min (r0,r1);
A6: min (r0,r1) > 0 by A4, A5, XXREAL_0:21;
( x0 - r0 <= x0 - (min (r0,r1)) & (f1 . x0) + (min (r0,r1)) <= (f1 . x0) + r1 ) by XREAL_1:6, XREAL_1:10, XXREAL_0:17;
then ( [.(x0 - (min (r0,r1))),x0.] c= [.(x0 - r0),x0.] & [.(f1 . x0),((f1 . x0) + (min (r0,r1))).] c= [.(f1 . x0),((f1 . x0) + r1).] ) by XXREAL_1:34;
then A7: [.(x0 - (min (r0,r1))),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) by A5;

A8: now :: thesis: for x being Real st x in [.(x0 - (min (r0,r1))),x0.] holds
x in dom (f2 * f1)

let x be Real; :: thesis: ( x in [.(x0 - (min (r0,r1))),x0.] implies x in dom (f2 * f1) )
assume x in [.(x0 - (min (r0,r1))),x0.] ; :: thesis: x in dom (f2 * f1)
then ( x in dom f1 & f1 . x in [.(f1 . x0),((f1 . x0) + r1).] ) by A7, FUNCT_1:54;
hence x in dom (f2 * f1) by A4, FUNCT_1:11; :: thesis: verum

end;

then A9: [.(x0 - (min (r0,r1))),x0.] c= dom (f2 * f1) ;
x0 - (min (r0,r1)) < x0 by A6, XREAL_1:44;
then A10: x0 in dom (f2 * f1) by A8, XXREAL_1:1;
then A11: f1 . x0 in dom f2 by FUNCT_1:11;
A12: dom (f2 * f1) c= dom f1 by RELAT_1:25;
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))) = (Rdiff (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))) = (Rdiff (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))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) )
assume that
A13: rng c = {x0} and
A14: rng (h + c) c= dom (f2 * f1) and
A15: 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))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )
A16: 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 A13, TARSKI:def 1; :: thesis: verum

end;

A17: 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 A18: x in rng (h + c) ; :: thesis: x in (left_open_halfline x0) /\ (dom f1)
then consider n being Element of NAT such that
A19: x = (h + c) . n by FUNCT_2:113;
dom (h + c) = NAT by FUNCT_2:def 1;
then x = (h . n) + (c . n) by A19, VALUED_1:def 1;
then x = (h . n) + x0 by A16;
then x < x0 by A15, XREAL_1:30;
then x in ].-infty,x0.[ by XXREAL_1:233;
then A20: x in left_open_halfline x0 by PROB_1:def 10;
x in dom f1 by A18, A14, FUNCT_1:11;
hence x in (left_open_halfline x0) /\ (dom f1) by A20, XBOOLE_0:def 4; :: thesis: verum

end;

then A21: rng (h + c) c= (left_open_halfline x0) /\ (dom f1) ;
set a = f1 /* c;
A22: rng c c= dom (f2 * f1) by A13, A10, ZFMISC_1:31;
set d = (f1 /* (h + c)) - (f1 /* c);
A23: lim h = 0 ;
lim c = c . 0 by SEQ_4:25;
then lim c = x0 by A16;
then A24: lim (h + c) = 0 + x0 by A23, SEQ_2:6
.= x0 ;
A25: f1 is_Lcontinuous_in x0 by A1, FDIFF_3:5;
then A26: f1 /* (h + c) is convergent by A21, A24, FDIFF_3:def 1;
A27: f1 . x0 = lim (f1 /* (h + c)) by A21, A24, A25, FDIFF_3:def 1;
A28: rng (f1 /* (h + c)) c= dom f2 by A14, 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
A29: (f1 /* c) . n = x by FUNCT_2:113;
c . n = x0 by A16;
then x = f1 . x0 by A29, A12, A13, A10, ZFMISC_1:31, FUNCT_2:108;
hence x in {(f1 . x0)} by TARSKI:def 1; :: thesis: verum

end;

then A30: 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) )
A31: (f1 /* c) . 0 in rng (f1 /* c) by VALUED_0:28;
assume x in {(f1 . x0)} ; :: thesis: x in rng (f1 /* c)
then A32: x = f1 . x0 by TARSKI:def 1;
c . 0 = x0 by A16;
hence x in rng (f1 /* c) by A32, A31, A12, A13, A10, ZFMISC_1:31, FUNCT_2:108; :: thesis: verum

end;

then {(f1 . x0)} c= rng (f1 /* c) ;
then A33: rng (f1 /* c) = {(f1 . x0)} by A30, XBOOLE_0:def 10;
then A34: rng (f1 /* c) c= dom f2 by A11, ZFMISC_1:31;

A35: 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 A36: (f1 /* c) . n = f1 . x0 by A30, TARSKI:def 1;
(f1 /* c) . (n + 1) in rng (f1 /* c) by VALUED_0:28;
hence (f1 /* c) . n = (f1 /* c) . (n + 1) by A30, A36, TARSKI:def 1; :: thesis: verum

end;

then A37: f1 /* c is constant by VALUED_0:25;
consider N being Nat such that
A38: for m being Nat st N <= m holds
|.(((h + c) . m) - (lim (h + c))).| < min (r0,r1) by A6, SEQ_2:def 7;
A39: ( rng ((h + c) ^\ N) c= rng (h + c) & rng (c ^\ N) c= rng c ) by NAT_1:55;
then A40: ( rng ((h + c) ^\ N) c= dom (f2 * f1) & rng (c ^\ N) c= dom (f2 * f1) ) by A14, A22;
then A41: ( rng (f1 /* ((h + c) ^\ N)) c= dom f2 & rng (f1 /* (c ^\ N)) c= dom f2 ) by FDIFF_2:9;
dom (f2 * f1) c= dom f1 by RELAT_1:25;
then A42: ( rng ((h + c) ^\ N) c= dom f1 & rng (c ^\ N) c= dom f1 ) by A39, A14, A22;
reconsider a = f1 /* c as constant Real_Sequence by A35, VALUED_0:25;
a . 0 in rng a by VALUED_0:28;
then a . 0 = f1 . x0 by A30, TARSKI:def 1;
then lim a = f1 . x0 by SEQ_4:25;
then A43: lim ((f1 /* (h + c)) - (f1 /* c)) = (f1 . x0) - (f1 . x0) by A26, A27, SEQ_2:12
.= 0 ;
( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (Rdiff (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))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

then consider k1 being Element of NAT such that
A44: for n being Element of NAT st k1 <= n holds
(f1 /* (h + c)) . n <> f1 . x0 ;
reconsider k = max (k1,N) as Element of NAT by ORDINAL1:def 12;
A45: ( k1 <= k & N <= k ) by XXREAL_0:25;

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

given n being Nat such that A47: (((f1 /* (h + c)) - (f1 /* c)) ^\ k) . n = 0 ; :: thesis: contradiction
A48: k + n is Element of NAT by ORDINAL1:def 12;
0 = ((f1 /* (h + c)) - (f1 /* c)) . (k + n) by A47, NAT_1:def 3
.= ((f1 /* (h + c)) . (k + n)) - ((f1 /* c) . (k + n)) by RFUNCT_2:1
.= ((f1 /* (h + c)) . (k + n)) - (f1 . (c . (k + n))) by A48, A12, A13, A10, ZFMISC_1:31, FUNCT_2:108
.= ((f1 /* (h + c)) . (n + k)) - (f1 . x0) by A16 ;
hence contradiction by A44, A45, 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)));

A49: 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 A37, A26, A43, SEQ_4:20;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) ^\ k as non-zero 0 -convergent Real_Sequence by A37, A26, A46, SEQ_1:5, FDIFF_1:def 1;
A50: for n being Nat holds d1 . n > 0

proof

let n be Nat; :: thesis: d1 . n > 0
A51: dom (h + c) = NAT by FUNCT_2:def 1;
A52: d1 . n = ((f1 /* (h + c)) - (f1 /* c)) . (k + n) by 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 A12, A13, A10, ZFMISC_1:31, FUNCT_2:108
.= ((f1 /* (h + c)) . (n + k)) - (f1 . x0) by A16
.= (f1 . ((h + c) . (n + k))) - (f1 . x0) by A21, XBOOLE_1:18, FUNCT_2:108 ;
(h + c) . (k + n) = (h . (k + n)) + (c . (k + n)) by A51, ORDINAL1:def 12, VALUED_1:def 1;
then A53: (h + c) . (k + n) = (h . (k + n)) + x0 by A16;
|.(((h + c) . (k + n)) - (lim (h + c))).| < min (r0,r1) by A38, A45, NAT_1:12;
then |.(((h . (k + n)) + (c . (k + n))) - x0).| < min (r0,r1) by A24, A51, ORDINAL1:def 12, VALUED_1:def 1;
then |.(((h . (k + n)) + x0) - x0).| < min (r0,r1) by A16;
then - (h . (k + n)) < min (r0,r1) by A15, ABSVALUE:def 1;
then - (- (h . (k + n))) > - (min (r0,r1)) by XREAL_1:24;
then ( x0 > (h + c) . (k + n) & (h + c) . (k + n) > x0 - (min (r0,r1)) ) by A53, A15, XREAL_1:8, XREAL_1:30;
then (h + c) . (k + n) in [.(x0 - (min (r0,r1))),x0.] by XXREAL_1:1;
then f1 . ((h + c) . (k + n)) in [.(f1 . x0),((f1 . x0) + r1).] by A7, FUNCT_1:54;
then A54: f1 . x0 <= f1 . ((h + c) . (k + n)) by XXREAL_1:1;
0 <> d1 . n by A46;
hence d1 . n > 0 by A54, A52, XREAL_1:48; :: thesis: verum

end;

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 A55: d1 + (a ^\ k) = (f1 /* (h + c)) ^\ k by A49, FUNCT_2:63;
rng ((f1 /* (h + c)) ^\ k) c= rng (f1 /* (h + c)) by VALUED_0:21;
then A56: rng (d1 + (a ^\ k)) c= dom f2 by A28, A55;
A57: rng (a ^\ k) = {(f1 . x0)} by A33, VALUED_0:26;
then A58: lim ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) = Rdiff (f2,(f1 . x0)) by A2, A50, A56, FDIFF_3:15;
Rdiff (f2,(f1 . x0)) = Rdiff (f2,(f1 . x0)) ;
then A59: (d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) is convergent by A2, A57, A56, A50, FDIFF_3:15;
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 A17;
then A60: 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 A61: rng ((h ^\ k) + (c ^\ k)) c= dom f1 by A60;
A62: rng (c ^\ k) = {x0} by A13, VALUED_0:26;
A63: 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 A15; :: thesis: verum

end;

Ldiff (f1,x0) = Ldiff (f1,x0) ;
then A64: ((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k))) is convergent by A1, A62, A63, A61, FDIFF_3:9;
A65: ((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 A21, XBOOLE_1:18, VALUED_0:27
.= ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) (#) ((((f1 /* (h + c)) ^\ k) - ((f1 /* c) ^\ k)) (#) ((h ^\ k) ")) by A12, A13, A10, ZFMISC_1:31, 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 A28, A55, VALUED_0:27
.= ((((f2 * f1) /* (h + c)) ^\ k) - (f2 /* (a ^\ k))) (#) ((h ^\ k) ") by A14, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) ^\ k) - ((f2 /* a) ^\ k)) (#) ((h ^\ k) ") by A33, A11, ZFMISC_1:31, VALUED_0:27
.= ((((f2 * f1) /* (h + c)) ^\ k) - (((f2 * f1) /* c) ^\ k)) (#) ((h ^\ k) ") by A13, A10, 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 A64, A59, SEQ_4:21; :: thesis: lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0))
lim (((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)))) = Ldiff (f1,x0) by A1, A62, A63, A61, FDIFF_3:9;
then lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A65, A64, A59, A58, SEQ_2:15;
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A64, A59, A65, SEQ_4:22; :: 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))) = (Rdiff (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 I1 being increasing sequence of NAT such that
A68: 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(A67);
reconsider h1 = h * I1 as non-zero 0 -convergent Real_Sequence by FDIFF_2:6;
set c1 = c * I1;
A69: c * I1 = c by VALUED_0:26;
A70: rng (c * I1) = {x0} by A13, VALUED_0:26;
A71: rng h1 c= rng h by VALUED_0:21;
A72: 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 h1 . n in rng h1 by FUNCT_1:3, ORDINAL1:def 12;
then ex m being Element of NAT st h1 . n = h . m by A71, FUNCT_2:113;
hence h1 . n < 0 by A15; :: thesis: verum

end;

reconsider c1 = c * I1 as constant Real_Sequence ;

A73: 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 A74: 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
A75: 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 A69, A75, A12, A13, A10, ZFMISC_1:31, FUNCT_2:108
.= |.(((h1 ") . m) * (((f1 /* (h1 + c1)) . m) - (f1 . x0))).| by A16
.= |.(((h1 ") . m) * (((f1 /* ((h + c) * I1)) . m) - (f1 . x0))).| by RFUNCT_2:2
.= |.(((h1 ") . m) * ((((f1 /* (h + c)) * I1) . m) - (f1 . x0))).| by A21, XBOOLE_1:18, FUNCT_2:110
.= |.(((h1 ") . m) * ((f1 . x0) - (f1 . x0))).| by A68
.= 0 by ABSVALUE:2 ;
hence |.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g by A74; :: thesis: verum

end;

rng ((h + c) * I1) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) * I1) c= dom f1 by A12, A14;
then A76: rng (h1 + c1) c= dom f1 by RFUNCT_2:2;
then A77: lim ((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) = Ldiff (f1,x0) by A1, A70, A72, FDIFF_3:9;
Ldiff (f1,x0) = Ldiff (f1,x0) ;
then (h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1)) is convergent by A1, A70, A76, A72, FDIFF_3:9;
then A78: Ldiff (f1,x0) = 0 by A77, A73, 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))) = (Rdiff (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)) . n = f1 . x0 or for k being Element of NAT ex n being Element of NAT st
( k <= n & (f1 /* ((h + c) ^\ N)) . 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)) . n = f1 . x0 ; :: thesis: ( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

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

A80: 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))) ^\ N) . m) - ((Rdiff (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))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g )
assume A81: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (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))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
let m be Nat; :: thesis: ( n <= m implies |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g )
A82: m in NAT by ORDINAL1:def 12;
assume A83: n <= m ; :: thesis: |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
|.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| = |.((((h ") ^\ N) (#) ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) ^\ N)) . m).| by A78, SEQM_3:19
.= |.((((h ") ^\ N) (#) ((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N))) . m).| by SEQM_3:17
.= |.((((h ") ^\ N) . m) * (((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N)) . m)).| by SEQ_1:8
.= |.((((h ") ^\ N) . m) * (((((f2 * f1) /* (h + c)) ^\ N) . m) - ((((f2 * f1) /* c) ^\ N) . m))).| by RFUNCT_2:1
.= |.((((h ") ^\ N) . m) * ((((f2 * f1) /* ((h + c) ^\ N)) . m) - ((((f2 * f1) /* c) ^\ N) . m))).| by A14, VALUED_0:27
.= |.((((h ") ^\ N) . m) * ((((f2 * f1) /* ((h + c) ^\ N)) . m) - (((f2 * f1) /* (c ^\ N)) . m))).| by A13, A10, ZFMISC_1:31, VALUED_0:27
.= |.((((h ") ^\ N) . m) * (((f2 /* (f1 /* ((h + c) ^\ N))) . m) - (((f2 * f1) /* (c ^\ N)) . m))).| by A40, VALUED_0:31
.= |.((((h ") ^\ N) . m) * (((f2 /* (f1 /* ((h + c) ^\ N))) . m) - ((f2 /* (f1 /* (c ^\ N))) . m))).| by A40, VALUED_0:31
.= |.((((h ") ^\ N) . m) * ((f2 . ((f1 /* ((h + c) ^\ N)) . m)) - ((f2 /* (f1 /* (c ^\ N))) . m))).| by A41, FUNCT_2:108, A82
.= |.((((h ") ^\ N) . m) * ((f2 . (f1 . x0)) - ((f2 /* (f1 /* (c ^\ N))) . m))).| by A83, A79, A82
.= |.((((h ") ^\ N) . m) * ((f2 . (f1 . x0)) - (f2 . ((f1 /* (c ^\ N)) . m)))).| by A82, A41, FUNCT_2:108
.= |.((((h ") ^\ N) . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . ((c ^\ N) . m))))).| by A42, FUNCT_2:108, A82
.= |.((((h ") ^\ N) . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . (c . (N + m)))))).| by NAT_1:def 3
.= |.((((h ") ^\ N) . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))).| by A16
.= 0 by ABSVALUE:2 ;
hence |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A81; :: thesis: verum

end;

then A84: ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N is convergent by SEQ_2:def 6;
then A85: lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A80, SEQ_2:def 7;
thus (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent by A84, SEQ_4:21; :: thesis: lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0))
thus lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A84, A85, SEQ_4:22; :: thesis: verum

end;

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

defpred S₂[ object ] means $1 <> f1 . x0;
A87: for k being Element of NAT ex n being Element of NAT st
( k <= n & S₂[(f1 /* ((h + c) ^\ N)) . n] ) by A86;
consider I2 being increasing sequence of NAT such that
A88: for n being Nat holds S₂[((f1 /* ((h + c) ^\ N)) * I2) . n] and
A89: for n being Element of NAT st ( for r being Real st r = (f1 /* ((h + c) ^\ N)) . n holds
S₂[r] ) holds
ex m being Element of NAT st n = I2 . m from FDIFF_2:sch 1(A87);
A90: ((f1 /* (h + c)) - (f1 /* c)) ^\ N = ((f1 /* (h + c)) ^\ N) - ((f1 /* c) ^\ N) by SEQM_3:17
.= (f1 /* ((h + c) ^\ N)) - ((f1 /* c) ^\ N) by A21, XBOOLE_1:18, VALUED_0:27
.= (f1 /* ((h + c) ^\ N)) - (f1 /* (c ^\ N)) by A12, A13, A10, ZFMISC_1:31, VALUED_0:27 ;
( rng (c ^\ N) c= rng c & rng ((h + c) ^\ N) c= rng (h + c) ) by VALUED_0:21;
then A91: ( rng (c ^\ N) c= dom f1 & rng ((h + c) ^\ N) c= dom f1 ) by A22, A12, A14;
A92: a ^\ N = f1 /* (c ^\ N) by A12, A13, A10, ZFMISC_1:31, VALUED_0:27;

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

given n being Nat such that A94: ((((f1 /* (h + c)) - (f1 /* c)) ^\ N) * I2) . n = 0 ; :: thesis: contradiction
0 = (((f1 /* (h + c)) - (f1 /* c)) ^\ N) . (I2 . n) by A94, FUNCT_2:15, ORDINAL1:def 12
.= ((f1 /* ((h + c) ^\ N)) . (I2 . n)) - ((f1 /* (c ^\ N)) . (I2 . n)) by A90, RFUNCT_2:1
.= ((f1 /* ((h + c) ^\ N)) . (I2 . n)) - (f1 . ((c ^\ N) . (I2 . n))) by A91, FUNCT_2:108
.= ((f1 /* ((h + c) ^\ N)) . (I2 . n)) - (f1 . (c . (N + (I2 . n)))) by NAT_1:def 3
.= ((f1 /* ((h + c) ^\ N)) . (I2 . n)) - (f1 . x0) by A16
.= (((f1 /* ((h + c) ^\ N)) * I2) . n) - (f1 . x0) by FUNCT_2:15, ORDINAL1:def 12 ;
hence contradiction by A88; :: thesis: verum

end;

reconsider h2 = (h ^\ N) * I2 as non-zero 0 -convergent Real_Sequence by FDIFF_2:6;
reconsider a1 = (a ^\ N) * I2 as constant Real_Sequence ;
reconsider c2 = (c ^\ N) * I2 as constant Real_Sequence ;
set s = (h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2));
(((f1 /* (h + c)) - (f1 /* c)) ^\ N) * I2 is subsequence of (f1 /* (h + c)) - (f1 /* c) by VALUED_0:20;
then lim ((((f1 /* (h + c)) - (f1 /* c)) ^\ N) * I2) = 0 by A37, A26, A43, SEQ_4:17;
then reconsider d1 = (((f1 /* (h + c)) - (f1 /* c)) ^\ N) * I2 as non-zero 0 -convergent Real_Sequence by A37, A26, SEQ_4:16, A93, SEQ_1:5, FDIFF_1:def 1;
set t = (d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1));
a1 is subsequence of a by VALUED_0:20;
then A95: rng a1 = {(f1 . x0)} by A33, VALUED_0:26;

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

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

end;

A97: rng ((f1 /* (h + c)) ^\ N) c= rng (f1 /* (h + c)) by VALUED_0:21;
then A98: rng ((f1 /* (h + c)) ^\ N) c= dom f2 by A28;
rng (a ^\ N) c= rng a by VALUED_0:21;
then A99: rng (a ^\ N) c= dom f2 by A34;
d1 + a1 = ((((f1 /* (h + c)) - (f1 /* c)) ^\ N) + (a ^\ N)) * I2 by RFUNCT_2:2;
then A100: d1 + a1 = (f1 /* ((h + c) ^\ N)) * I2 by A96, FUNCT_2:63
.= ((f1 /* (h + c)) ^\ N) * I2 by A21, XBOOLE_1:18, VALUED_0:27 ;
A101: h2 + c2 = ((h ^\ N) + (c ^\ N)) * I2 by RFUNCT_2:2
.= ((h + c) ^\ N) * I2 by SEQM_3:15 ;
A102: ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) (#) ((h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2))) = ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) (#) ((((f1 /* ((h + c) ^\ N)) * I2) - (f1 /* c2)) (#) (h2 ")) by A91, A101, FUNCT_2:110
.= ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) (#) ((((f1 /* ((h + c) ^\ N)) * I2) - ((f1 /* (c ^\ N)) * I2)) (#) (h2 ")) by A91, FUNCT_2:110
.= (((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) ((((f1 /* ((h + c) ^\ N)) * I2) - ((f1 /* (c ^\ N)) * I2)) (#) (h2 ")) by VALUED_1:def 10
.= (((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) (((((f1 /* (h + c)) ^\ N) * I2) - ((f1 /* (c ^\ N)) * I2)) (#) (h2 ")) by A21, XBOOLE_1:18, VALUED_0:27
.= (((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) (((((f1 /* (h + c)) ^\ N) * I2) - (((f1 /* c) ^\ N) * I2)) (#) (h2 ")) by A12, A13, A10, ZFMISC_1:31, VALUED_0:27
.= (((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) (((((f1 /* (h + c)) ^\ N) - ((f1 /* c) ^\ N)) * I2) (#) (h2 ")) by RFUNCT_2:2
.= (((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) (d1 (#) (h2 ")) by SEQM_3:17
.= ((((f2 /* (d1 + a1)) - (f2 /* a1)) /" d1) (#) d1) (#) (h2 ") by SEQ_1:14
.= ((f2 /* (((f1 /* (h + c)) ^\ N) * I2)) - (f2 /* a1)) (#) (h2 ") by A100, SEQ_1:37
.= (((f2 /* ((f1 /* (h + c)) ^\ N)) * I2) - (f2 /* a1)) (#) (h2 ") by A98, FUNCT_2:110
.= ((((f2 /* (f1 /* (h + c))) ^\ N) * I2) - (f2 /* a1)) (#) (h2 ") by A28, VALUED_0:27
.= (((((f2 * f1) /* (h + c)) ^\ N) * I2) - (f2 /* a1)) (#) (h2 ") by A14, VALUED_0:31
.= (((((f2 * f1) /* (h + c)) ^\ N) * I2) - ((f2 /* (a ^\ N)) * I2)) (#) (h2 ") by A99, FUNCT_2:110
.= (((((f2 * f1) /* (h + c)) ^\ N) * I2) - (((f2 /* a) ^\ N) * I2)) (#) (h2 ") by A33, A11, ZFMISC_1:31, VALUED_0:27
.= (((((f2 * f1) /* (h + c)) ^\ N) * I2) - ((((f2 * f1) /* c) ^\ N) * I2)) (#) (h2 ") by A13, A10, ZFMISC_1:31, VALUED_0:31
.= (((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N)) * I2) (#) (h2 ") by RFUNCT_2:2
.= (((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N)) * I2) (#) (((h ^\ N) ") * I2) by RFUNCT_2:5
.= (((h ^\ N) ") (#) ((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N))) * I2 by RFUNCT_2:2 ;
rng (((f1 /* (h + c)) ^\ N) * I2) c= rng ((f1 /* (h + c)) ^\ N) by VALUED_0:21;
then A103: rng (d1 + a1) c= dom f2 by A97, A28, A100;
((h + c) ^\ N) * I2 is subsequence of h + c by VALUED_0:20;
then rng (((h + c) ^\ N) * I2) c= rng (h + c) by VALUED_0:21;
then rng (((h + c) ^\ N) * I2) c= dom f1 by A12, A14;
then rng (((h ^\ N) + (c ^\ N)) * I2) c= dom f1 by SEQM_3:15;
then A104: rng (h2 + c2) c= dom f1 by RFUNCT_2:2;
h2 is subsequence of h by VALUED_0:20;
then A105: rng h2 c= rng h by VALUED_0:21;
A106: 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 A105, FUNCT_2:113;
hence h2 . n < 0 by A15; :: thesis: verum

end;

c2 is subsequence of c by VALUED_0:20;
then A107: rng c2 = {x0} by A13, VALUED_0:26;
then A108: lim ((h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2))) = Ldiff (f1,x0) by A1, A104, A106, FDIFF_3:9;
A109: for n being Nat holds d1 . n > 0

proof

let n be Nat; :: thesis: d1 . n > 0
n in NAT by ORDINAL1:def 12;
then A110: n in dom I2 by FUNCT_2:def 1;
then A111: ((f1 /* ((h + c) ^\ N)) * I2) . n = (f1 /* ((h + c) ^\ N)) . (I2 . n) by FUNCT_1:13
.= f1 . (((h + c) ^\ N) . (I2 . n)) by A42, FUNCT_2:108 ;
A112: d1 . n = ((f1 /* ((h + c) ^\ N)) - (f1 /* (c ^\ N))) . (I2 . n) by A90, A110, FUNCT_1:13
.= ((f1 /* ((h + c) ^\ N)) . (I2 . n)) - ((f1 /* (c ^\ N)) . (I2 . n)) by RFUNCT_2:1
.= ((f1 /* ((h + c) ^\ N)) . (I2 . n)) - (f1 . ((c ^\ N) . (I2 . n))) by A42, FUNCT_2:108
.= ((f1 /* ((h + c) ^\ N)) . (I2 . n)) - (f1 . (c . (N + (I2 . n)))) by NAT_1:def 3
.= ((f1 /* ((h + c) ^\ N)) . (I2 . n)) - (f1 . x0) by A16
.= (f1 . (((h + c) ^\ N) . (I2 . n))) - (f1 . x0) by A42, FUNCT_2:108 ;
A113: ((h + c) ^\ N) . (I2 . n) = (h + c) . (N + (I2 . n)) by NAT_1:def 3;
then A114: ((h + c) ^\ N) . (I2 . n) = (h . (N + (I2 . n))) + (c . (N + (I2 . n))) by SEQ_1:7
.= (h . (N + (I2 . n))) + x0 by A16 ;
|.((((h + c) ^\ N) . (I2 . n)) - x0).| < min (r0,r1) by A113, A24, A38, NAT_1:12;
then - (h . (N + (I2 . n))) < min (r0,r1) by A15, A114, ABSVALUE:def 1;
then - (- (h . (N + (I2 . n)))) > - (min (r0,r1)) by XREAL_1:24;
then ( x0 - (min (r0,r1)) < ((h + c) ^\ N) . (I2 . n) & ((h + c) ^\ N) . (I2 . n) < x0 ) by A114, A15, XREAL_1:8, XREAL_1:30;
then ((h + c) ^\ N) . (I2 . n) in [.(x0 - (min (r0,r1))),x0.] by XXREAL_1:1;
then f1 . (((h + c) ^\ N) . (I2 . n)) in [.(f1 . x0),((f1 . x0) + r1).] by A7, FUNCT_1:54;
then f1 . x0 <= f1 . (((h + c) ^\ N) . (I2 . n)) by XXREAL_1:1;
then f1 . x0 < f1 . (((h + c) ^\ N) . (I2 . n)) by A88, A111, XXREAL_0:1;
hence d1 . n > 0 by A112, XREAL_1:50; :: thesis: verum

end;

Ldiff (f1,x0) = Ldiff (f1,x0) ;
then A115: (h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2)) is convergent by A1, A107, A104, A106, FDIFF_3:9;
Rdiff (f2,(f1 . x0)) = Rdiff (f2,(f1 . x0)) ;
then A116: (d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1)) is convergent by A2, A95, A103, A109, FDIFF_3:15;
lim ((d1 ") (#) ((f2 /* (d1 + a1)) - (f2 /* a1))) = Rdiff (f2,(f1 . x0)) by A2, A95, A103, A109, FDIFF_3:15;
then A117: lim ((((h ^\ N) ") (#) ((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N))) * I2) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A102, A115, A108, A116, SEQ_2:15;

A118: 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))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g

set DF = (Rdiff (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))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g )
assume A119: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
consider k being Nat such that
A120: for m being Nat st k <= m holds
|.((((((h ^\ N) ") (#) ((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N))) * I2) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A102, A115, A116, A117, A119, SEQ_2:def 7;
A121: 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))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
let m be Nat; :: thesis: ( n <= m implies |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g )
assume A122: n <= m ; :: thesis: |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g
A123: m in NAT by ORDINAL1:def 12;
A124: ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N = ((h ") ^\ N) (#) ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) ^\ N) by SEQM_3:19
.= ((h ^\ N) ") (#) ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) ^\ N) by SEQM_3:18
.= ((h ^\ N) ") (#) ((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N)) by SEQM_3:17 ;

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

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

suppose A125: (f1 /* ((h + c) ^\ N)) . m = f1 . x0 ; :: thesis: |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g

A126: (((h ^\ N) ") (#) ((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N))) . m = (((h ^\ N) ") . m) * (((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N)) . m) by SEQ_1:8;
A127: ((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N)) . m = ((((f2 * f1) /* (h + c)) ^\ N) . m) - ((((f2 * f1) /* c) ^\ N) . m) by RFUNCT_2:1;
dom ((h + c) ^\ N) = NAT by FUNCT_2:def 1;
then dom (f1 * ((h + c) ^\ N)) = NAT by A91, RELAT_1:27;
then dom (f1 /* ((h + c) ^\ N)) = NAT by A91, FUNCT_2:def 11;
then A128: dom (f2 * (f1 /* ((h + c) ^\ N))) = NAT by A41, RELAT_1:27;
((f2 * f1) /* (h + c)) ^\ N = (f2 * f1) /* ((h + c) ^\ N) by A14, VALUED_0:27
.= f2 /* (f1 /* ((h + c) ^\ N)) by A40, VALUED_0:31
.= f2 * (f1 /* ((h + c) ^\ N)) by A41, FUNCT_2:def 11 ;
then A129: (((f2 * f1) /* (h + c)) ^\ N) . m = f2 . (f1 . x0) by A125, A128, FUNCT_1:12, ORDINAL1:def 12;
dom (c ^\ N) = NAT by FUNCT_2:def 1;
then dom (f1 * (c ^\ N)) = NAT by A91, RELAT_1:27;
then dom (f1 /* (c ^\ N)) = NAT by A91, FUNCT_2:def 11;
then A130: dom (f2 * (f1 /* (c ^\ N))) = NAT by A41, RELAT_1:27;
((f2 * f1) /* c) ^\ N = (f2 * f1) /* (c ^\ N) by A13, A10, ZFMISC_1:31, VALUED_0:27
.= f2 /* (f1 /* (c ^\ N)) by A40, VALUED_0:31
.= f2 * (f1 /* (c ^\ N)) by A41, FUNCT_2:def 11 ;
then (((f2 * f1) /* c) ^\ N) . m = f2 . ((f1 /* (c ^\ N)) . m) by ORDINAL1:def 12, A130, FUNCT_1:12
.= f2 . (f1 . ((c ^\ N) . m)) by A123, A91, FUNCT_2:108
.= f2 . (f1 . (c . (N + m))) by NAT_1:def 3
.= f2 . (f1 . x0) by A16 ;
hence |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A124, A119, A78, A126, A129, A127, ABSVALUE:2; :: thesis: verum

end;

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

then for r1 being Real st (f1 /* ((h + c) ^\ N)) . m = r1 holds
r1 <> f1 . x0 ;
then consider l being Element of NAT such that
A131: m = I2 . l by A89, A123;
dom I2 = NAT by FUNCT_2:def 1;
then l >= k by A122, A131, VALUED_0:def 13, A121;
then |.((((((h ^\ N) ") (#) ((((f2 * f1) /* (h + c)) ^\ N) - (((f2 * f1) /* c) ^\ N))) * I2) . l) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A120;
hence |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) . m) - ((Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)))).| < g by A124, A131, FUNCT_2:15; :: thesis: verum

end;

end;

end;

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

end;

then A132: ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N is convergent by SEQ_2:def 6;
hence (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent by SEQ_4:21; :: thesis: lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0))
lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ N) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A118, A132, SEQ_2:def 7;
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) by A132, SEQ_4:22; :: 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))) = (Rdiff (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))) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) ) ; :: thesis: verum

end;

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