let x0 be Real; :: thesis:
let f2, f1 be PartFunc of REAL,REAL; :: thesis:
given N being Neighbourhood of x0 such that A1: N c= dom (f2 * f1) ; :: thesis:
assume that
A2: f1 is_differentiable_in x0 and
A3: f2 is_differentiable_in f1 . x0 ; :: thesis:
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f2 * f1) holds
( (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent & lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) )

let h be convergent_to_0 Real_Sequence; :: thesis:
let c be V8() Real_Sequence; :: thesis:
assume that
A4: rng c = {x0} and
A5: rng (h + c) c= dom (f2 * f1) ; :: thesis:
A6: rng (h + c) c= dom f1 by A5, Th9;
set a = f1 /* c;

A7: now

let n be Element of NAT ; :: thesis:
c . n in rng c by VALUED_0:28;
hence c . n = x0 by A4, TARSKI:def 1; :: thesis:

end;

A8: rng c c= dom (f2 * f1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng c ; :: thesis:
then A9: ex n being Element of NAT st c . n = x by FUNCT_2:113;
x0 in N by RCOMP_1:16;
then x0 in dom (f2 * f1) by A1;
hence x in dom (f2 * f1) by A7, A9; :: thesis:

end;

set d = (f1 /* (h + c)) - (f1 /* c);
A10: lim h = 0 by FDIFF_1:def 1;
A11: h is convergent by FDIFF_1:def 1;
then A12: h + c is convergent by SEQ_2:5;
lim c = c . 0 by SEQ_4:25;
then lim c = x0 by A7;
then A13: lim (h + c) = 0 + x0 by A11, A10, SEQ_2:6
.= x0 ;
A14: f1 is_continuous_in x0 by A2, FDIFF_1:24;
then A15: f1 /* (h + c) is convergent by A6, A12, A13, FCONT_1:def 1;
A16: f1 . x0 = lim (f1 /* (h + c)) by A6, A12, A13, A14, FCONT_1:def 1;
A17: rng (f1 /* (h + c)) c= dom f2 by A5, Th9;
A18: rng c c= dom f1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng c ; :: thesis:
then A19: x = x0 by A4, TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence x in dom f1 by A1, A19, FUNCT_1:11; :: thesis:

end;

A20: rng (f1 /* c) = {(f1 . x0)}

proof

thus rng (f1 /* c) c= {(f1 . x0)} :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (f1 /* c) ; :: thesis:
then consider n being Element of NAT such that
A21: (f1 /* c) . n = x by FUNCT_2:113;
c . n = x0 by A7;
then x = f1 . x0 by A18, A21, FUNCT_2:108;
hence x in {(f1 . x0)} by TARSKI:def 1; :: thesis:

end;

let x be set ; :: according to TARSKI:def 3 :: thesis:
A22: (f1 /* c) . 0 in rng (f1 /* c) by VALUED_0:28;
assume x in {(f1 . x0)} ; :: thesis:
then A23: x = f1 . x0 by TARSKI:def 1;
c . 0 = x0 by A7;
hence x in rng (f1 /* c) by A18, A23, A22, FUNCT_2:108; :: thesis:

end;

A24: rng (f1 /* c) c= dom f2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (f1 /* c) ; :: thesis:
then A25: x = f1 . x0 by A20, TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence x in dom f2 by A1, A25, FUNCT_1:11; :: thesis:

end;

A26: now

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

end;

then f1 /* c is constant by VALUED_0:25;
then A28: (f1 /* (h + c)) - (f1 /* c) is convergent by A15, SEQ_2:11;
reconsider a = f1 /* c as V8() Real_Sequence by A26, VALUED_0:25;
a . 0 in rng a by VALUED_0:28;
then a . 0 = f1 . x0 by A20, TARSKI:def 1;
then lim a = f1 . x0 by SEQ_4:25;
then A29: lim ((f1 /* (h + c)) - (f1 /* c)) = (f1 . x0) - (f1 . x0) by A15, A16, 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))) * (diff (f1,x0)) )

proof

per cases ;

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:

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

now

given n being Element of NAT such that A31: (((f1 /* (h + c)) - (f1 /* c)) ^\ k) . n = 0 ; :: thesis:
0 = ((f1 /* (h + c)) - (f1 /* c)) . (n + k) by A31, 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 A18, FUNCT_2:108
.= ((f1 /* (h + c)) . (n + k)) - (f1 . x0) by A7 ;
hence contradiction by A30, NAT_1:12; :: thesis:

end;

then A32: ((f1 /* (h + c)) - (f1 /* c)) ^\ k is non-empty by SEQ_1:5;
set c1 = c ^\ k;
set h1 = h ^\ k;
set a1 = a ^\ k;
set s = ((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)));

A33: now

let n be Element of NAT ; :: thesis:
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:

end;

lim (((f1 /* (h + c)) - (f1 /* c)) ^\ k) = 0 by A28, A29, SEQ_4:20;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) ^\ k as convergent_to_0 Real_Sequence by A28, A32, 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 A34: d1 + (a ^\ k) = (f1 /* (h + c)) ^\ k by A33, FUNCT_2:63;
rng ((f1 /* (h + c)) ^\ k) c= rng (f1 /* (h + c)) by VALUED_0:21;
then A35: rng (d1 + (a ^\ k)) c= dom f2 by A17, A34, XBOOLE_1:1;
A36: rng (a ^\ k) = {(f1 . x0)} by A20, VALUED_0:26;
then A37: lim ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) = diff (f2,(f1 . x0)) by A3, A35, Th12;
diff (f2,(f1 . x0)) = diff (f2,(f1 . x0)) ;
then A38: (d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) is convergent by A3, A36, A35, Th12;
rng ((h + c) ^\ k) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) ^\ k) c= dom f1 by A6, XBOOLE_1:1;
then A39: rng ((h ^\ k) + (c ^\ k)) c= dom f1 by SEQM_3:15;
A40: rng (c ^\ k) = {x0} by A4, VALUED_0:26;
diff (f1,x0) = diff (f1,x0) ;
then A41: ((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k))) is convergent by A2, A40, A39, Th12;
A42: ((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 A6, VALUED_0:27
.= ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) (#) ((((f1 /* (h + c)) ^\ k) - ((f1 /* c) ^\ k)) (#) ((h ^\ k) ")) by A18, VALUED_0:27
.= (((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 A32, SEQ_1:37
.= (((f2 /* (f1 /* (h + c))) ^\ k) - (f2 /* (a ^\ k))) (#) ((h ^\ k) ") by A17, A34, VALUED_0:27
.= ((((f2 * f1) /* (h + c)) ^\ k) - (f2 /* (a ^\ k))) (#) ((h ^\ k) ") by A5, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) ^\ k) - ((f2 /* a) ^\ k)) (#) ((h ^\ k) ") by A24, VALUED_0:27
.= ((((f2 * f1) /* (h + c)) ^\ k) - (((f2 * f1) /* c) ^\ k)) (#) ((h ^\ k) ") by A8, 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 ;
then A43: ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k is convergent by A41, A38, SEQ_2:14;
hence (h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent by SEQ_4:21; :: thesis:
lim (((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)))) = diff (f1,x0) by A2, A40, A39, Th12;
then lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A42, A41, A38, A37, SEQ_2:15;
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A43, SEQ_4:22; :: thesis:

end;

suppose A44: for k being Element of NAT ex n being Element of NAT st
( k <= n & (f1 /* (h + c)) . n = f1 . x0 ) ; :: thesis:

defpred S₁[ set ] means $1 = f1 . x0;
A45: for k being Element of NAT ex n being Element of NAT st
( k <= n & S₁[(f1 /* (h + c)) . n] ) by A44;
consider I1 being V36() sequence of NAT such that
A46: for n being Element of 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(A45);
h * I1 is subsequence of h by VALUED_0:def 17;
then reconsider h1 = h * I1 as convergent_to_0 Real_Sequence by Th6;
set c1 = c * I1;
A47: c * I1 is subsequence of c by VALUED_0:def 17;
then A48: c * I1 = c by VALUED_0:26;
A49: rng (c * I1) = {x0} by A4, A47, VALUED_0:26;
reconsider c1 = c * I1 as V8() Real_Sequence ;

A50: now

let g be real number ; :: thesis:
assume A51: 0 < g ; :: thesis:
take n = 0 ; :: thesis:
let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
abs ((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0) = abs (((h1 ") . m) * (((f1 /* (h1 + c1)) - (f1 /* c1)) . m)) by SEQ_1:8
.= abs (((h1 ") . m) * (((f1 /* (h1 + c1)) . m) - ((f1 /* c1) . m))) by RFUNCT_2:1
.= abs (((h1 ") . m) * (((f1 /* (h1 + c1)) . m) - (f1 . (c . m)))) by A18, A48, FUNCT_2:108
.= abs (((h1 ") . m) * (((f1 /* (h1 + c1)) . m) - (f1 . x0))) by A7
.= abs (((h1 ") . m) * (((f1 /* ((h + c) * I1)) . m) - (f1 . x0))) by RFUNCT_2:2
.= abs (((h1 ") . m) * ((((f1 /* (h + c)) * I1) . m) - (f1 . x0))) by A6, FUNCT_2:110
.= abs (((h1 ") . m) * ((f1 . x0) - (f1 . x0))) by A46
.= 0 by ABSVALUE:2 ;
hence abs ((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0) < g by A51; :: thesis:

end;

(h + c) * I1 is subsequence of h + c by VALUED_0:def 17;
then rng ((h + c) * I1) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) * I1) c= dom f1 by A6, XBOOLE_1:1;
then A52: rng (h1 + c1) c= dom f1 by RFUNCT_2:2;
then A53: lim ((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) = diff (f1,x0) by A2, A49, Th12;
diff (f1,x0) = diff (f1,x0) ;
then (h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1)) is convergent by A2, A49, A52, Th12;
then A54: diff (f1,x0) = 0 by A53, A50, SEQ_2:def 7;

now

per cases ;

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:

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

A56: now

let g be real number ; :: thesis:
assume A57: 0 < g ; :: thesis:
take n = k; :: thesis:
let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
then A58: (f1 /* (h + c)) . m = f1 . x0 by A55;
abs ((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))) = abs (((h ") . m) * ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) . m)) by A54, SEQ_1:8
.= abs (((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (((f2 * f1) /* c) . m))) by RFUNCT_2:1
.= abs (((h ") . m) * (((f2 /* (f1 /* (h + c))) . m) - (((f2 * f1) /* c) . m))) by A5, VALUED_0:31
.= abs (((h ") . m) * ((f2 . ((f1 /* (h + c)) . m)) - (((f2 * f1) /* c) . m))) by A17, FUNCT_2:108
.= abs (((h ") . m) * ((f2 . (f1 . x0)) - ((f2 /* (f1 /* c)) . m))) by A8, A58, VALUED_0:31
.= abs (((h ") . m) * ((f2 . (f1 . x0)) - (f2 . ((f1 /* c) . m)))) by A24, FUNCT_2:108
.= abs (((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . (c . m))))) by A18, FUNCT_2:108
.= abs (((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))) by A7
.= 0 by ABSVALUE:2 ;
hence abs ((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))) < g by A57; :: thesis:

end;

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

end;

suppose A59: for k being Element of NAT ex n being Element of NAT st
( k <= n & (f1 /* (h + c)) . n <> f1 . x0 ) ; :: thesis:

defpred S₂[ set ] means $1 <> f1 . x0;
A60: for k being Element of NAT ex n being Element of NAT st
( k <= n & S₂[(f1 /* (h + c)) . n] ) by A59;
consider I2 being V36() sequence of NAT such that
A61: for n being Element of NAT holds S₂[((f1 /* (h + c)) * I2) . n] and
A62: 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(A60);

now

given n being Element of NAT such that A63: (((f1 /* (h + c)) - (f1 /* c)) * I2) . n = 0 ; :: thesis:
0 = ((f1 /* (h + c)) - (f1 /* c)) . (I2 . n) by A63, 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 A18, FUNCT_2:108
.= ((f1 /* (h + c)) . (I2 . n)) - (f1 . x0) by A7
.= (((f1 /* (h + c)) * I2) . n) - (f1 . x0) by FUNCT_2:15 ;
hence contradiction by A61; :: thesis:

end;

then A64: ((f1 /* (h + c)) - (f1 /* c)) * I2 is non-empty by SEQ_1:5;
h * I2 is subsequence of h by VALUED_0:def 17;
then reconsider h2 = h * I2 as convergent_to_0 Real_Sequence by Th6;
set a1 = a * I2;
set c2 = c * I2;
reconsider c2 = c * I2 as V8() Real_Sequence ;
set s = (h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2));
A65: ((f1 /* (h + c)) - (f1 /* c)) * I2 is subsequence of (f1 /* (h + c)) - (f1 /* c) by VALUED_0:def 17;
then A66: ((f1 /* (h + c)) - (f1 /* c)) * I2 is convergent by A28, SEQ_4:16;
lim (((f1 /* (h + c)) - (f1 /* c)) * I2) = 0 by A28, A29, A65, SEQ_4:17;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) * I2 as convergent_to_0 Real_Sequence by A66, A64, FDIFF_1:def 1;
set t = (d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)));
a * I2 is subsequence of a by VALUED_0:def 17;
then A67: rng (a * I2) = {(f1 . x0)} by A20, VALUED_0:26;

A68: now

end;

d1 + (a * I2) = (((f1 /* (h + c)) - (f1 /* c)) + a) * I2 by RFUNCT_2:2;
then A69: d1 + (a * I2) = (f1 /* (h + c)) * I2 by A68, FUNCT_2:63;
A70: ((d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) (#) ((h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2))) = ((d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) (#) (((f1 /* ((h + c) * I2)) - (f1 /* c2)) (#) (h2 ")) by RFUNCT_2:2
.= ((d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) (#) ((((f1 /* (h + c)) * I2) - (f1 /* c2)) (#) (h2 ")) by A6, FUNCT_2:110
.= ((d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) (#) ((((f1 /* (h + c)) * I2) - ((f1 /* c) * I2)) (#) (h2 ")) by A18, FUNCT_2:110
.= (((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) /" d1) (#) (d1 (#) (h2 ")) by RFUNCT_2:2
.= ((((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) /" d1) (#) d1) (#) (h2 ") by SEQ_1:14
.= ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) (#) (h2 ") by A64, SEQ_1:37
.= (((f2 /* (f1 /* (h + c))) * I2) - (f2 /* (a * I2))) (#) (h2 ") by A17, A69, FUNCT_2:110
.= ((((f2 * f1) /* (h + c)) * I2) - (f2 /* (a * I2))) (#) (h2 ") by A5, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) * I2) - ((f2 /* a) * I2)) (#) (h2 ") by A24, FUNCT_2:110
.= ((((f2 * f1) /* (h + c)) * I2) - (((f2 * f1) /* c) * I2)) (#) (h2 ") by A8, 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 ;
reconsider a1 = a * I2 as V8() Real_Sequence ;
(f1 /* (h + c)) * I2 is subsequence of f1 /* (h + c) by VALUED_0:def 17;
then rng ((f1 /* (h + c)) * I2) c= rng (f1 /* (h + c)) by VALUED_0:21;
then A71: rng (d1 + a1) c= dom f2 by A17, A69, XBOOLE_1:1;
(h + c) * I2 is subsequence of h + c by VALUED_0:def 17;
then rng ((h + c) * I2) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) * I2) c= dom f1 by A6, XBOOLE_1:1;
then A72: rng (h2 + c2) c= dom f1 by RFUNCT_2:2;
c2 is subsequence of c by VALUED_0:def 17;
then A73: rng c2 = {x0} by A4, VALUED_0:26;
then A74: lim ((h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2))) = diff (f1,x0) by A2, A72, Th12;
diff (f1,x0) = diff (f1,x0) ;
then A75: (h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2)) is convergent by A2, A73, A72, Th12;
diff (f2,(f1 . x0)) = diff (f2,(f1 . x0)) ;
then A76: (d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) is convergent by A3, A67, A71, Th12;
then A77: ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2 is convergent by A70, A75, SEQ_2:14;
lim ((d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) = diff (f2,(f1 . x0)) by A3, A67, A71, Th12;
then A78: lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A70, A75, A74, A76, SEQ_2:15;

A79: now

set DF = (diff (f2,(f1 . x0))) * (diff (f1,x0));
let g be real number ; :: thesis:
assume A80: 0 < g ; :: thesis:
consider k being Element of NAT such that
A81: for m being Element of NAT st k <= m holds
abs (((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))) < g by A77, A78, A80, SEQ_2:def 7;
take n = I2 . k; :: thesis:
let m be Element of NAT ; :: thesis:
assume A82: n <= m ; :: thesis:

now

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

suppose A83: (f1 /* (h + c)) . m = f1 . x0 ; :: thesis:

abs ((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))) = abs (((h ") . m) * ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) . m)) by A54, SEQ_1:8
.= abs (((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (((f2 * f1) /* c) . m))) by RFUNCT_2:1
.= abs (((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - ((f2 /* (f1 /* c)) . m))) by A8, VALUED_0:31
.= abs (((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . ((f1 /* c) . m)))) by A24, FUNCT_2:108
.= abs (((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . (f1 . (c . m))))) by A18, FUNCT_2:108
.= abs (((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . (f1 . x0)))) by A7
.= abs (((h ") . m) * (((f2 /* (f1 /* (h + c))) . m) - (f2 . (f1 . x0)))) by A5, VALUED_0:31
.= abs (((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))) by A17, A83, FUNCT_2:108
.= 0 by ABSVALUE:2 ;
hence abs ((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))) < g by A80; :: thesis:

end;

suppose (f1 /* (h + c)) . m <> f1 . x0 ; :: thesis:

then for r1 being Real st (f1 /* (h + c)) . m = r1 holds
r1 <> f1 . x0 ;
then consider l being Element of NAT such that
A84: m = I2 . l by A62;
dom I2 = NAT by FUNCT_2:def 1;
then l >= k by A82, A84, VALUED_0:def 13;
then abs (((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) . l) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))) < g by A81;
hence abs ((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))) < g by A84, FUNCT_2:15; :: thesis:

end;

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

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))) * (diff (f1,x0)) ) ; :: thesis:

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))) * (diff (f1,x0)) ) ; :: thesis:

end;

hence ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) ) by A1, Th12; :: thesis: