let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st ex N being Neighbourhood of x0 st N c= dom (f2 * f1) & f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( ex N being Neighbourhood of x0 st N c= dom (f2 * f1) & f1 is_differentiable_in x0 & f2 is_differentiable_in f1 . x0 implies ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) ) )
given N being Neighbourhood of x0 such that A1: N c= dom (f2 * f1) ; :: thesis: ( not f1 is_differentiable_in x0 or not f2 is_differentiable_in f1 . x0 or ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) ) )
assume that
A2: f1 is_differentiable_in x0 and
A3: f2 is_differentiable_in f1 . x0 ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) )
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) 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)) )

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) 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 c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f2 * f1) implies ( (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)) ) )
assume that
A4: rng c = {x0} and
A5: rng (h + c) c= dom (f2 * f1) ; :: thesis: ( (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)) )
A6: rng (h + c) c= dom f1 by A5, Th9;
set a = f1 /* c;

A7: now :: thesis: for n being Element of NAT holds c . n = x0

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in dom (f2 * f1) )
assume x in rng c ; :: thesis: x in dom (f2 * f1)
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: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in dom f1 )
assume x in rng c ; :: thesis: x in dom f1
then A17: x = x0 by A4, TARSKI:def 1;
x0 in N by RCOMP_1:16;
hence x in dom f1 by A1, A17, FUNCT_1:11; :: thesis: verum

end;

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

proof

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

proof

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f1 . x0)} or x in rng (f1 /* c) )
A20: (f1 /* c) . 0 in rng (f1 /* c) by VALUED_0:28;
assume x in {(f1 . x0)} ; :: thesis: x in rng (f1 /* c)
then A21: x = f1 . x0 by TARSKI:def 1;
c . 0 = x0 by A7;
hence x in rng (f1 /* c) by A16, A21, A20, FUNCT_2:108; :: thesis: verum

end;

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

proof

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

end;

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

end;

then f1 /* c is constant by VALUED_0:25;
then A26: (f1 /* (h + c)) - (f1 /* c) is convergent by A13;
reconsider a = f1 /* c as constant Real_Sequence by A24, VALUED_0:25;
a . 0 in rng a by VALUED_0:28;
then a . 0 = f1 . x0 by A18, TARSKI:def 1;
then lim a = f1 . x0 by SEQ_4:25;
then A27: lim ((f1 /* (h + c)) - (f1 /* c)) = (f1 . x0) - (f1 . x0) by A13, A14, 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 ( 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))) * (diff (f1,x0)) )

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

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

given n being Nat such that A29: (((f1 /* (h + c)) - (f1 /* c)) ^\ k) . n = 0 ; :: thesis: contradiction
0 = ((f1 /* (h + c)) - (f1 /* c)) . (n + k) by A29, 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 A16, FUNCT_2:108
.= ((f1 /* (h + c)) . (n + k)) - (f1 . x0) by A7 ;
hence contradiction by A28, NAT_1:12; :: thesis: verum

end;

then A30: ((f1 /* (h + c)) - (f1 /* c)) ^\ k is non-zero 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)));

A31: 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 A26, A27, SEQ_4:20;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) ^\ k as non-zero 0 -convergent Real_Sequence by A26, A30, 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 A32: d1 + (a ^\ k) = (f1 /* (h + c)) ^\ k by A31, FUNCT_2:63;
rng ((f1 /* (h + c)) ^\ k) c= rng (f1 /* (h + c)) by VALUED_0:21;
then A33: rng (d1 + (a ^\ k)) c= dom f2 by A15, A32;
A34: rng (a ^\ k) = {(f1 . x0)} by A18, VALUED_0:26;
then A35: lim ((d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) = diff (f2,(f1 . x0)) by A3, A33, Th12;
diff (f2,(f1 . x0)) = diff (f2,(f1 . x0)) ;
then A36: (d1 ") (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) is convergent by A3, A34, A33, Th12;
rng ((h + c) ^\ k) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) ^\ k) c= dom f1 by A6;
then A37: rng ((h ^\ k) + (c ^\ k)) c= dom f1 by SEQM_3:15;
A38: rng (c ^\ k) = {x0} by A4, VALUED_0:26;
diff (f1,x0) = diff (f1,x0) ;
then A39: ((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k))) is convergent by A2, A38, A37, Th12;
A40: ((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 A16, 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 SEQ_1:37
.= (((f2 /* (f1 /* (h + c))) ^\ k) - (f2 /* (a ^\ k))) (#) ((h ^\ k) ") by A15, A32, 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 A22, 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 A41: ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k is convergent by A39, A36;
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))) = (diff (f2,(f1 . x0))) * (diff (f1,x0))
lim (((h ^\ k) ") (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)))) = diff (f1,x0) by A2, A38, A37, Th12;
then lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A40, A39, A36, A35, SEQ_2:15;
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A41, SEQ_4:22; :: thesis: verum

end;

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

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

A48: 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 A49: 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
A50: 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 A16, A46, A50, FUNCT_2:108
.= |.(((h1 ") . m) * (((f1 /* (h1 + c1)) . m) - (f1 . x0))).| by A7, A50
.= |.(((h1 ") . m) * (((f1 /* ((h + c) * I1)) . m) - (f1 . x0))).| by RFUNCT_2:2
.= |.(((h1 ") . m) * ((((f1 /* (h + c)) * I1) . m) - (f1 . x0))).| by A6, FUNCT_2:110
.= |.(((h1 ") . m) * ((f1 . x0) - (f1 . x0))).| by A44
.= 0 by ABSVALUE:2 ;
hence |.((((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0).| < g by A49; :: thesis: verum

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;
then A51: rng (h1 + c1) c= dom f1 by RFUNCT_2:2;
then A52: lim ((h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) = diff (f1,x0) by A2, A47, Th12;
diff (f1,x0) = diff (f1,x0) ;
then (h1 ") (#) ((f1 /* (h1 + c1)) - (f1 /* c1)) is convergent by A2, A47, A51, Th12;
then A53: diff (f1,x0) = 0 by A52, A48, 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))) * (diff (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))) * (diff (f1,x0)) )

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

A55: 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))) * (diff (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))) * (diff (f1,x0)))).| < g )
assume A56: 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))) * (diff (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))) * (diff (f1,x0)))).| < g
let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g )
A57: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g
then A58: (f1 /* (h + c)) . m = f1 . x0 by A54, A57;
|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| = |.(((h ") . m) * ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) . m)).| by A53, 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 A5, VALUED_0:31
.= |.(((h ") . m) * ((f2 . ((f1 /* (h + c)) . m)) - (((f2 * f1) /* c) . m))).| by A15, FUNCT_2:108, A57
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - ((f2 /* (f1 /* c)) . m))).| by A8, A58, VALUED_0:31
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - (f2 . ((f1 /* c) . m)))).| by A22, FUNCT_2:108, A57
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . (c . m))))).| by A16, FUNCT_2:108, A57
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))).| by A7, A57
.= 0 by ABSVALUE:2 ;
hence |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g by A56; :: 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))) * (diff (f1,x0))
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A55, SEQ_2:def 7; :: thesis: verum

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

defpred S₂[ object ] 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 increasing sequence of NAT such that
A61: for n being 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 :: thesis: for n being Nat holds not (((f1 /* (h + c)) - (f1 /* c)) * I2) . n = 0

given n being Nat such that A63: (((f1 /* (h + c)) - (f1 /* c)) * I2) . n = 0 ; :: thesis: contradiction
A64: n in NAT by ORDINAL1:def 12;
then 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 A16, FUNCT_2:108
.= ((f1 /* (h + c)) . (I2 . n)) - (f1 . x0) by A7
.= (((f1 /* (h + c)) * I2) . n) - (f1 . x0) by FUNCT_2:15, A64 ;
hence contradiction by A61; :: thesis: verum

end;

then A65: ((f1 /* (h + c)) - (f1 /* c)) * I2 is non-zero by SEQ_1:5;
h * I2 is subsequence of h by VALUED_0:def 17;
then reconsider h2 = h * I2 as non-zero 0 -convergent Real_Sequence by Th6;
set a1 = a * I2;
set c2 = c * I2;
reconsider c2 = c * I2 as constant Real_Sequence ;
set s = (h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2));
A66: ((f1 /* (h + c)) - (f1 /* c)) * I2 is subsequence of (f1 /* (h + c)) - (f1 /* c) by VALUED_0:def 17;
then A67: ((f1 /* (h + c)) - (f1 /* c)) * I2 is convergent by A26, SEQ_4:16;
lim (((f1 /* (h + c)) - (f1 /* c)) * I2) = 0 by A26, A27, A66, SEQ_4:17;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) * I2 as non-zero 0 -convergent Real_Sequence by A67, A65, 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 A68: rng (a * I2) = {(f1 . x0)} by A18, VALUED_0:26;

A69: 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 + (a * I2) = (((f1 /* (h + c)) - (f1 /* c)) + a) * I2 by RFUNCT_2:2;
then A70: d1 + (a * I2) = (f1 /* (h + c)) * I2 by A69, FUNCT_2:63;
A71: ((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 A16, 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 SEQ_1:37
.= (((f2 /* (f1 /* (h + c))) * I2) - (f2 /* (a * I2))) (#) (h2 ") by A15, A70, 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 A22, 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 constant 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 A72: rng (d1 + a1) c= dom f2 by A15, A70;
(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;
then A73: rng (h2 + c2) c= dom f1 by RFUNCT_2:2;
c2 is subsequence of c by VALUED_0:def 17;
then A74: rng c2 = {x0} by A4, VALUED_0:26;
then A75: lim ((h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2))) = diff (f1,x0) by A2, A73, Th12;
diff (f1,x0) = diff (f1,x0) ;
then A76: (h2 ") (#) ((f1 /* (h2 + c2)) - (f1 /* c2)) is convergent by A2, A74, A73, Th12;
diff (f2,(f1 . x0)) = diff (f2,(f1 . x0)) ;
then A77: (d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) is convergent by A3, A68, A72, Th12;
then A78: ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2 is convergent by A71, A76;
lim ((d1 ") (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) = diff (f2,(f1 . x0)) by A3, A68, A72, Th12;
then A79: lim (((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A71, A76, A75, A77, SEQ_2:15;

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))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g

set DF = (diff (f2,(f1 . x0))) * (diff (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))) * (diff (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))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g
consider k being Nat such that
A82: for m being Nat st k <= m holds
|.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g by A78, A79, A81, SEQ_2:def 7;
A83: 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))) * (diff (f1,x0)))).| < g
let m be Nat; :: thesis: ( n <= m implies |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g )
assume A84: n <= m ; :: thesis: |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g
A85: m in NAT by ORDINAL1:def 12;

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

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

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

|.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| = |.(((h ") . m) * ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) . m)).| by A53, 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 A22, FUNCT_2:108, A85
.= |.(((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . (f1 . (c . m))))).| by A16, FUNCT_2:108, A85
.= |.(((h ") . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . (f1 . x0)))).| by A7, A85
.= |.(((h ") . m) * (((f2 /* (f1 /* (h + c))) . m) - (f2 . (f1 . x0)))).| by A5, VALUED_0:31
.= |.(((h ") . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))).| by A15, A86, FUNCT_2:108, A85
.= 0 by ABSVALUE:2 ;
hence |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g by A81; :: thesis: verum

end;

suppose (f1 /* (h + c)) . m <> f1 . x0 ; :: thesis: |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (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
A87: m = I2 . l by A62, A85;
dom I2 = NAT by FUNCT_2:def 1;
then l >= k by A84, A87, VALUED_0:def 13, A83;
then |.(((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) . l) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g by A82;
hence |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (f1,x0)))).| < g by A87, FUNCT_2:15; :: thesis: verum

end;

end;

end;

hence |.((((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff (f2,(f1 . x0))) * (diff (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))) * (diff (f1,x0))
hence lim ((h ") (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff (f2,(f1 . x0))) * (diff (f1,x0)) by A80, 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))) * (diff (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))) * (diff (f1,x0)) ) ; :: thesis: verum

end;

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