let x0 be Real; :: thesis: for f2, f1 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 f2, f1 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 A2: ( f1 is_differentiable_in x0 & 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 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) )
proof
let h be convergent_to_0 Real_Sequence; :: thesis: 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 c be V8() 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 A3: ( rng c = {x0} & 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) )
then A4: ( rng (h + c) c= dom f1 & rng (f1 /* (h + c)) c= dom f2 ) by Th9;
A5: now
let n be Element of NAT ; :: thesis: c . n = x0
c . n in rng c by VALUED_0:28;
hence c . n = x0 by A3, TARSKI:def 1; :: thesis: verum
end;
set a = f1 /* c;
A6: rng c c= dom f1
proof
let x be set ; :: 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 A7: x = x0 by A3, TARSKI:def 1;
x0 in N by RCOMP_1:37;
hence x in dom f1 by A1, A7, FUNCT_1:21; :: thesis: verum
end;
A8: 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 set ; :: 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
A9: (f1 /* c) . n = x by FUNCT_2:190;
c . n = x0 by A5;
then x = f1 . x0 by A6, A9, FUNCT_2:185;
hence x in {(f1 . x0)} by TARSKI:def 1; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(f1 . x0)} or x in rng (f1 /* c) )
assume x in {(f1 . x0)} ; :: thesis: x in rng (f1 /* c)
then A10: x = f1 . x0 by TARSKI:def 1;
A11: c . 0 = x0 by A5;
(f1 /* c) . 0 in rng (f1 /* c) by VALUED_0:28;
hence x in rng (f1 /* c) by A6, A10, A11, FUNCT_2:185; :: thesis: verum
end;
A12: rng c c= dom (f2 * f1)
proof
let x be set ; :: 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 A13: ex n being Element of NAT st c . n = x by FUNCT_2:190;
x0 in N by RCOMP_1:37;
then x0 in dom (f2 * f1) by A1;
hence x in dom (f2 * f1) by A5, A13; :: thesis: verum
end;
A14: rng (f1 /* c) c= dom f2
proof
let x be set ; :: 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 A15: x = f1 . x0 by A8, TARSKI:def 1;
x0 in N by RCOMP_1:37;
hence x in dom f2 by A1, A15, FUNCT_1:21; :: thesis: verum
end;
A16: now
let n be Nat; :: thesis: (f1 /* c) . n = (f1 /* c) . (n + 1)
( (f1 /* c) . n in rng (f1 /* c) & (f1 /* c) . (n + 1) in rng (f1 /* c) ) by VALUED_0:28;
then ( (f1 /* c) . n = f1 . x0 & (f1 /* c) . (n + 1) = f1 . x0 ) by A8, TARSKI:def 1;
hence (f1 /* c) . n = (f1 /* c) . (n + 1) ; :: thesis: verum
end;
then A17: f1 /* c is constant by VALUED_0:25;
reconsider a = f1 /* c as V8() Real_Sequence by A16, VALUED_0:25;
lim c = c . 0 by SEQ_4:40;
then A19: lim c = x0 by A5;
A20: ( h is convergent & lim h = 0 & h is non-zero ) by FDIFF_1:def 1;
then A21: h + c is convergent by SEQ_2:19;
A22: lim (h + c) = 0 + x0 by A19, A20, SEQ_2:20
.= x0 ;
f1 is_continuous_in x0 by A2, FDIFF_1:32;
then A23: ( f1 /* (h + c) is convergent & f1 . x0 = lim (f1 /* (h + c)) ) by A4, A21, A22, FCONT_1:def 1;
A24: f1 /* c is convergent by A17;
a . 0 in rng a by VALUED_0:28;
then a . 0 = f1 . x0 by A8, TARSKI:def 1;
then A25: lim a = f1 . x0 by SEQ_4:40;
set d = (f1 /* (h + c)) - (f1 /* c);
A26: (f1 /* (h + c)) - (f1 /* c) is convergent by A23, A24, SEQ_2:25;
A27: lim ((f1 /* (h + c)) - (f1 /* c)) = (f1 . x0) - (f1 . x0) by A23, A25, SEQ_2:26
.= 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 ;
A29: ( ((f1 /* (h + c)) - (f1 /* c)) ^\ k is convergent & lim (((f1 /* (h + c)) - (f1 /* c)) ^\ k) = 0 ) by A26, A27, SEQ_4:33;
now
given n being Element of NAT such that A30: (((f1 /* (h + c)) - (f1 /* c)) ^\ k) . n = 0 ; :: thesis: contradiction
0 = ((f1 /* (h + c)) - (f1 /* c)) . (n + k) by A30, NAT_1:def 3
.= ((f1 /* (h + c)) . (n + k)) - ((f1 /* c) . (n + k)) by RFUNCT_2:6
.= ((f1 /* (h + c)) . (n + k)) - (f1 . (c . (n + k))) by A6, FUNCT_2:185
.= ((f1 /* (h + c)) . (n + k)) - (f1 . x0) by A5 ;
hence contradiction by A28, NAT_1:12; :: thesis: verum
end;
then A31: ((f1 /* (h + c)) - (f1 /* c)) ^\ k is non-zero by SEQ_1:7;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) ^\ k as convergent_to_0 Real_Sequence by A29, FDIFF_1:def 1;
set a1 = a ^\ k;
set h1 = h ^\ k;
set c1 = c ^\ k;
set t = (d1 " ) (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)));
set s = ((h ^\ k) " ) (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)));
A32: d1 + (a ^\ k) = (f1 /* (h + c)) ^\ k
proof
A33: d1 + (a ^\ k) = (((f1 /* (h + c)) - (f1 /* c)) + a) ^\ k by SEQM_3:37;
now
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:11
.= (((f1 /* (h + c)) . n) - (a . n)) + (a . n) by RFUNCT_2:6
.= (f1 /* (h + c)) . n ; :: thesis: verum
end;
hence d1 + (a ^\ k) = (f1 /* (h + c)) ^\ k by A33, FUNCT_2:113; :: thesis: verum
end;
A34: ((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:37
.= ((d1 " ) (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) (#) ((((f1 /* (h + c)) ^\ k) - (f1 /* (c ^\ k))) (#) ((h ^\ k) " )) by A4, VALUED_0:27
.= ((d1 " ) (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) (#) ((((f1 /* (h + c)) ^\ k) - ((f1 /* c) ^\ k)) (#) ((h ^\ k) " )) by A6, VALUED_0:27
.= (((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) /" d1) (#) (d1 (#) ((h ^\ k) " )) by SEQM_3:39
.= ((((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) /" d1) (#) d1) (#) ((h ^\ k) " ) by SEQ_1:22
.= ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) (#) ((h ^\ k) " ) by A31, SEQ_1:45
.= (((f2 /* (f1 /* (h + c))) ^\ k) - (f2 /* (a ^\ k))) (#) ((h ^\ k) " ) by A4, A32, VALUED_0:27
.= ((((f2 * f1) /* (h + c)) ^\ k) - (f2 /* (a ^\ k))) (#) ((h ^\ k) " ) by A3, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) ^\ k) - ((f2 /* a) ^\ k)) (#) ((h ^\ k) " ) by A14, VALUED_0:27
.= ((((f2 * f1) /* (h + c)) ^\ k) - (((f2 * f1) /* c) ^\ k)) (#) ((h ^\ k) " ) by A12, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) ^\ k) (#) ((h ^\ k) " ) by SEQM_3:39
.= ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) ^\ k) (#) ((h " ) ^\ k) by SEQM_3:41
.= ((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k by SEQM_3:42 ;
A35: ( rng (c ^\ k) = {x0} & diff f1,x0 = diff f1,x0 ) by A3, VALUED_0:26;
rng ((h + c) ^\ k) c= rng (h + c) by VALUED_0:21;
then rng ((h + c) ^\ k) c= dom f1 by A4, XBOOLE_1:1;
then rng ((h ^\ k) + (c ^\ k)) c= dom f1 by SEQM_3:37;
then A36: ( ((h ^\ k) " ) (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k))) is convergent & lim (((h ^\ k) " ) (#) ((f1 /* ((h ^\ k) + (c ^\ k))) - (f1 /* (c ^\ k)))) = diff f1,x0 ) by A2, A35, Th12;
A37: ( rng (a ^\ k) = {(f1 . x0)} & diff f2,(f1 . x0) = diff f2,(f1 . x0) ) by A8, VALUED_0:26;
rng ((f1 /* (h + c)) ^\ k) c= rng (f1 /* (h + c)) by VALUED_0:21;
then rng (d1 + (a ^\ k)) c= dom f2 by A4, A32, XBOOLE_1:1;
then A38: ( (d1 " ) (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k))) is convergent & lim ((d1 " ) (#) ((f2 /* (d1 + (a ^\ k))) - (f2 /* (a ^\ k)))) = diff f2,(f1 . x0) ) by A2, A37, Th12;
then A39: ((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k is convergent by A34, A36, SEQ_2:28;
hence (h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) is convergent by SEQ_4:35; :: thesis: lim ((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff f2,(f1 . x0)) * (diff f1,x0)
lim (((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) ^\ k) = (diff f2,(f1 . x0)) * (diff f1,x0) by A34, A36, A38, SEQ_2:29;
hence lim ((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) = (diff f2,(f1 . x0)) * (diff f1,x0) by A39, SEQ_4:36; :: thesis: verum
end;
suppose A40: 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 S1[ set ] means $1 = f1 . x0;
A41: for k being Element of NAT ex n being Element of NAT st
( k <= n & S1[(f1 /* (h + c)) . n] ) by A40;
consider I1 being V35() sequence of NAT such that
A42: for n being Element of NAT holds S1[((f1 /* (h + c)) * I1) . n] and
for n being Element of NAT st ( for r being Real st r = (f1 /* (h + c)) . n holds
S1[r] ) holds
ex m being Element of NAT st n = I1 . m from FDIFF_2:sch 1(A41);
set c1 = c * I1;
A43: c * I1 is subsequence of c by VALUED_0:def 17;
then A44: c * I1 = c by VALUED_0:26;
A45: ( rng (c * I1) = {x0} & diff f1,x0 = diff f1,x0 ) by A3, A43, VALUED_0:26;
reconsider c1 = c * I1 as V8() Real_Sequence ;
h * I1 is subsequence of h by VALUED_0:def 17;
then reconsider h1 = h * I1 as convergent_to_0 Real_Sequence by Th6;
(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 A4, XBOOLE_1:1;
then rng (h1 + c1) c= dom f1 by RFUNCT_2:13;
then A46: ( (h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1)) is convergent & lim ((h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) = diff f1,x0 ) by A2, A45, Th12;
now
let g be real number ; :: thesis: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0 ) < g )
assume A47: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0 ) < g
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs ((((h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0 ) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0 ) < g )
assume n <= m ; :: thesis: abs ((((h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0 ) < g
abs ((((h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0 ) = abs (((h1 " ) . m) * (((f1 /* (h1 + c1)) - (f1 /* c1)) . m)) by SEQ_1:12
.= abs (((h1 " ) . m) * (((f1 /* (h1 + c1)) . m) - ((f1 /* c1) . m))) by RFUNCT_2:6
.= abs (((h1 " ) . m) * (((f1 /* (h1 + c1)) . m) - (f1 . (c . m)))) by A6, A44, FUNCT_2:185
.= abs (((h1 " ) . m) * (((f1 /* (h1 + c1)) . m) - (f1 . x0))) by A5
.= abs (((h1 " ) . m) * (((f1 /* ((h + c) * I1)) . m) - (f1 . x0))) by RFUNCT_2:13
.= abs (((h1 " ) . m) * ((((f1 /* (h + c)) * I1) . m) - (f1 . x0))) by A4, FUNCT_2:187
.= abs (((h1 " ) . m) * ((f1 . x0) - (f1 . x0))) by A42
.= 0 by ABSVALUE:7 ;
hence abs ((((h1 " ) (#) ((f1 /* (h1 + c1)) - (f1 /* c1))) . m) - 0 ) < g by A47; :: thesis: verum
end;
then A48: diff f1,x0 = 0 by A46, SEQ_2:def 7;
now
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
A49: for n being Element of NAT st k <= n holds
(f1 /* (h + c)) . n = f1 . x0 ;
A50: now
let g be real number ; :: thesis: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g )
assume A51: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g
take n = k; :: thesis: for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g )
assume n <= m ; :: thesis: abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g
then A52: (f1 /* (h + c)) . m = f1 . x0 by A49;
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 A48, SEQ_1:12
.= abs (((h " ) . m) * ((((f2 * f1) /* (h + c)) . m) - (((f2 * f1) /* c) . m))) by RFUNCT_2:6
.= abs (((h " ) . m) * (((f2 /* (f1 /* (h + c))) . m) - (((f2 * f1) /* c) . m))) by A3, VALUED_0:31
.= abs (((h " ) . m) * ((f2 . ((f1 /* (h + c)) . m)) - (((f2 * f1) /* c) . m))) by A4, FUNCT_2:185
.= abs (((h " ) . m) * ((f2 . (f1 . x0)) - ((f2 /* (f1 /* c)) . m))) by A12, A52, VALUED_0:31
.= abs (((h " ) . m) * ((f2 . (f1 . x0)) - (f2 . ((f1 /* c) . m)))) by A14, FUNCT_2:185
.= abs (((h " ) . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . (c . m))))) by A6, FUNCT_2:185
.= abs (((h " ) . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))) by A5
.= 0 by ABSVALUE:7 ;
hence abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g by A51; :: 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 A50, SEQ_2:def 7; :: thesis: verum
end;
suppose A53: 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 S2[ set ] means $1 <> f1 . x0;
A54: for k being Element of NAT ex n being Element of NAT st
( k <= n & S2[(f1 /* (h + c)) . n] ) by A53;
consider I2 being V35() sequence of NAT such that
A55: for n being Element of NAT holds S2[((f1 /* (h + c)) * I2) . n] and
A56: for n being Element of NAT st ( for r being Real st r = (f1 /* (h + c)) . n holds
S2[r] ) holds
ex m being Element of NAT st n = I2 . m from FDIFF_2:sch 1(A54);
set c2 = c * I2;
reconsider c2 = c * I2 as V8() Real_Sequence ;
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 s = (h2 " ) (#) ((f1 /* (h2 + c2)) - (f1 /* c2));
A57: ((f1 /* (h + c)) - (f1 /* c)) * I2 is subsequence of (f1 /* (h + c)) - (f1 /* c) by VALUED_0:def 17;
then A58: ((f1 /* (h + c)) - (f1 /* c)) * I2 is convergent by A26, SEQ_4:29;
A59: lim (((f1 /* (h + c)) - (f1 /* c)) * I2) = 0 by A26, A27, A57, SEQ_4:30;
now
given n being Element of NAT such that A60: (((f1 /* (h + c)) - (f1 /* c)) * I2) . n = 0 ; :: thesis: contradiction
0 = ((f1 /* (h + c)) - (f1 /* c)) . (I2 . n) by A60, FUNCT_2:21
.= ((f1 /* (h + c)) . (I2 . n)) - ((f1 /* c) . (I2 . n)) by RFUNCT_2:6
.= ((f1 /* (h + c)) . (I2 . n)) - (f1 . (c . (I2 . n))) by A6, FUNCT_2:185
.= ((f1 /* (h + c)) . (I2 . n)) - (f1 . x0) by A5
.= (((f1 /* (h + c)) * I2) . n) - (f1 . x0) by FUNCT_2:21 ;
hence contradiction by A55; :: thesis: verum
end;
then A61: ((f1 /* (h + c)) - (f1 /* c)) * I2 is non-zero by SEQ_1:7;
then reconsider d1 = ((f1 /* (h + c)) - (f1 /* c)) * I2 as convergent_to_0 Real_Sequence by A58, A59, FDIFF_1:def 1;
set a1 = a * I2;
set t = (d1 " ) (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)));
A62: d1 + (a * I2) = (f1 /* (h + c)) * I2
proof
A63: d1 + (a * I2) = (((f1 /* (h + c)) - (f1 /* c)) + a) * I2 by RFUNCT_2:13;
now
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:11
.= (((f1 /* (h + c)) . n) - (a . n)) + (a . n) by RFUNCT_2:6
.= (f1 /* (h + c)) . n ; :: thesis: verum
end;
hence d1 + (a * I2) = (f1 /* (h + c)) * I2 by A63, FUNCT_2:113; :: thesis: verum
end;
A64: ((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:13
.= ((d1 " ) (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) (#) ((((f1 /* (h + c)) * I2) - (f1 /* c2)) (#) (h2 " )) by A4, FUNCT_2:187
.= ((d1 " ) (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) (#) ((((f1 /* (h + c)) * I2) - ((f1 /* c) * I2)) (#) (h2 " )) by A6, FUNCT_2:187
.= (((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) /" d1) (#) (d1 (#) (h2 " )) by RFUNCT_2:13
.= ((((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) /" d1) (#) d1) (#) (h2 " ) by SEQ_1:22
.= ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) (#) (h2 " ) by A61, SEQ_1:45
.= (((f2 /* (f1 /* (h + c))) * I2) - (f2 /* (a * I2))) (#) (h2 " ) by A4, A62, FUNCT_2:187
.= ((((f2 * f1) /* (h + c)) * I2) - (f2 /* (a * I2))) (#) (h2 " ) by A3, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) * I2) - ((f2 /* a) * I2)) (#) (h2 " ) by A14, FUNCT_2:187
.= ((((f2 * f1) /* (h + c)) * I2) - (((f2 * f1) /* c) * I2)) (#) (h2 " ) by A12, VALUED_0:31
.= ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) * I2) (#) (h2 " ) by RFUNCT_2:13
.= ((((f2 * f1) /* (h + c)) - ((f2 * f1) /* c)) * I2) (#) ((h " ) * I2) by RFUNCT_2:16
.= ((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2 by RFUNCT_2:13 ;
c2 is subsequence of c by VALUED_0:def 17;
then A65: ( rng c2 = {x0} & diff f1,x0 = diff f1,x0 ) by A3, VALUED_0:26;
(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 A4, XBOOLE_1:1;
then rng (h2 + c2) c= dom f1 by RFUNCT_2:13;
then A66: ( (h2 " ) (#) ((f1 /* (h2 + c2)) - (f1 /* c2)) is convergent & lim ((h2 " ) (#) ((f1 /* (h2 + c2)) - (f1 /* c2))) = diff f1,x0 ) by A2, A65, Th12;
a * I2 is subsequence of a by VALUED_0:def 17;
then A68: ( rng (a * I2) = {(f1 . x0)} & diff f2,(f1 . x0) = diff f2,(f1 . x0) ) by A8, VALUED_0:26;
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 rng (d1 + a1) c= dom f2 by A4, A62, XBOOLE_1:1;
then A69: ( (d1 " ) (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2))) is convergent & lim ((d1 " ) (#) ((f2 /* (d1 + (a * I2))) - (f2 /* (a * I2)))) = diff f2,(f1 . x0) ) by A2, A68, Th12;
then A70: ((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2 is convergent by A64, A66, SEQ_2:28;
A71: lim (((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) * I2) = (diff f2,(f1 . x0)) * (diff f1,x0) by A64, A66, A69, SEQ_2:29;
A72: now
let g be real number ; :: thesis: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g )
assume A73: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((((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);
consider k being Element of NAT such that
A74: 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 A70, A71, A73, SEQ_2:def 7;
take n = I2 . k; :: thesis: for m being Element of NAT st n <= m holds
abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g )
assume A75: n <= m ; :: thesis: abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g
now
per cases ( (f1 /* (h + c)) . m = f1 . x0 or (f1 /* (h + c)) . m <> f1 . x0 ) ;
suppose A76: (f1 /* (h + c)) . m = f1 . x0 ; :: thesis: abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g
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 A48, SEQ_1:12
.= abs (((h " ) . m) * ((((f2 * f1) /* (h + c)) . m) - (((f2 * f1) /* c) . m))) by RFUNCT_2:6
.= abs (((h " ) . m) * ((((f2 * f1) /* (h + c)) . m) - ((f2 /* (f1 /* c)) . m))) by A12, VALUED_0:31
.= abs (((h " ) . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . ((f1 /* c) . m)))) by A14, FUNCT_2:185
.= abs (((h " ) . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . (f1 . (c . m))))) by A6, FUNCT_2:185
.= abs (((h " ) . m) * ((((f2 * f1) /* (h + c)) . m) - (f2 . (f1 . x0)))) by A5
.= abs (((h " ) . m) * (((f2 /* (f1 /* (h + c))) . m) - (f2 . (f1 . x0)))) by A3, VALUED_0:31
.= abs (((h " ) . m) * ((f2 . (f1 . x0)) - (f2 . (f1 . x0)))) by A4, A76, FUNCT_2:185
.= 0 by ABSVALUE:7 ;
hence abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g by A73; :: thesis: verum
end;
suppose (f1 /* (h + c)) . m <> f1 . x0 ; :: thesis: abs ((((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
A77: m = I2 . l by A56;
dom I2 = NAT by FUNCT_2:def 1;
then l >= k by A75, A77, 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 A74;
hence abs ((((h " ) (#) (((f2 * f1) /* (h + c)) - ((f2 * f1) /* c))) . m) - ((diff f2,(f1 . x0)) * (diff f1,x0))) < g by A77, FUNCT_2:21; :: thesis: verum
end;
end;
end;
hence abs ((((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 A72, 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