let f1, f2 be PartFunc of REAL,REAL; :: thesis: for x0 being Real st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 holds
( f1 (#) f2 is_left_differentiable_in x0 & Ldiff ((f1 (#) f2),x0) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) )
let x0 be Real; :: thesis: ( f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in x0 implies ( f1 (#) f2 is_left_differentiable_in x0 & Ldiff ((f1 (#) f2),x0) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) ) )
assume that
A1: f1 is_left_differentiable_in x0 and
A2: f2 is_left_differentiable_in x0 ; :: thesis: ( f1 (#) f2 is_left_differentiable_in x0 & Ldiff ((f1 (#) f2),x0) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) )
consider r2 being Real such that
A3: 0 < r2 and
A4: [.(x0 - r2),x0.] c= dom f2 by A2;
consider r1 being Real such that
A5: 0 < r1 and
A6: [.(x0 - r1),x0.] c= dom f1 by A1;
set r = min (r1,r2);
A7: 0 < min (r1,r2) by A5, A3, XXREAL_0:15;
then A8: x0 - (min (r1,r2)) <= x0 by XREAL_1:43;
min (r1,r2) <= r2 by XXREAL_0:17;
then A9: x0 - r2 <= x0 - (min (r1,r2)) by XREAL_1:13;
then x0 - r2 <= x0 by A8, XXREAL_0:2;
then A10: x0 in [.(x0 - r2),x0.] by XXREAL_1:1;
x0 - (min (r1,r2)) in { g where g is Real : ( x0 - r2 <= g & g <= x0 ) } by A8, A9;
then x0 - (min (r1,r2)) in [.(x0 - r2),x0.] by RCOMP_1:def 1;
then [.(x0 - (min (r1,r2))),x0.] c= [.(x0 - r2),x0.] by A10, XXREAL_2:def 12;
then A11: [.(x0 - (min (r1,r2))),x0.] c= dom f2 by A4;
min (r1,r2) <= r1 by XXREAL_0:17;
then A12: x0 - r1 <= x0 - (min (r1,r2)) by XREAL_1:13;
then x0 - r1 <= x0 by A8, XXREAL_0:2;
then A13: x0 in [.(x0 - r1),x0.] by XXREAL_1:1;
x0 - (min (r1,r2)) in { g where g is Real : ( x0 - r1 <= g & g <= x0 ) } by A8, A12;
then x0 - (min (r1,r2)) in [.(x0 - r1),x0.] by RCOMP_1:def 1;
then [.(x0 - (min (r1,r2))),x0.] c= [.(x0 - r1),x0.] by A13, XXREAL_2:def 12;
then A14: [.(x0 - (min (r1,r2))),x0.] c= dom f1 by A6;
A15: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {x0} & rng (h + c) c= dom (f1 (#) f2) & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) is convergent & lim ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (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 (f1 (#) f2) & ( for n being Nat holds h . n < 0 ) holds
( (h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) is convergent & lim ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) )
let c be constant Real_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= dom (f1 (#) f2) & ( for n being Nat holds h . n < 0 ) implies ( (h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) is convergent & lim ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) ) )
assume that
A16: rng c = {x0} and
A17: rng (h + c) c= dom (f1 (#) f2) and
A18: for n being Nat holds h . n < 0 ; :: thesis: ( (h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) is convergent & lim ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) )
A19: rng (h + c) c= (dom f1) /\ (dom f2) by A17, VALUED_1:def 4;

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

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

end;

then A20: (f1 /* c) + ((f1 /* (h + c)) - (f1 /* c)) = f1 /* (h + c) by FUNCT_2:63;
A21: for m being Element of NAT holds c . m = x0

proof

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

end;

0 <= min (r1,r2) by A5, A3, XXREAL_0:15;
then x0 - (min (r1,r2)) <= x0 by XREAL_1:43;
then A22: x0 in [.(x0 - (min (r1,r2))),x0.] by XXREAL_1:1;
then A23: x0 in dom f1 by A14;
A24: rng c c= dom f1 by A16, A23, TARSKI:def 1;
A25: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f1 /* c) . m) - (f1 . x0)).| < g

proof

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
|.(((f1 /* c) . m) - (f1 . x0)).| < g )
assume A26: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((f1 /* c) . m) - (f1 . x0)).| < g
take n = 0 ; :: thesis: for m being Nat st n <= m holds
|.(((f1 /* c) . m) - (f1 . x0)).| < g
let m be Nat; :: thesis: ( n <= m implies |.(((f1 /* c) . m) - (f1 . x0)).| < g )
assume n <= m ; :: thesis: |.(((f1 /* c) . m) - (f1 . x0)).| < g
A27: m in NAT by ORDINAL1:def 12;
|.(((f1 /* c) . m) - (f1 . x0)).| = |.((f1 . (c . m)) - (f1 . x0)).| by A24, FUNCT_2:108, A27
.= |.((f1 . x0) - (f1 . x0)).| by A21, A27
.= 0 by ABSVALUE:def 1 ;
hence |.(((f1 /* c) . m) - (f1 . x0)).| < g by A26; :: thesis: verum

end;

then A28: f1 /* c is convergent by SEQ_2:def 6;
A29: x0 in dom f2 by A11, A22;
A30: rng c c= dom f2 by A16, A29, TARSKI:def 1;
A31: for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((f2 /* c) . m) - (f2 . x0)).| < g

proof

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
|.(((f2 /* c) . m) - (f2 . x0)).| < g )
assume A32: 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((f2 /* c) . m) - (f2 . x0)).| < g
take n = 0 ; :: thesis: for m being Nat st n <= m holds
|.(((f2 /* c) . m) - (f2 . x0)).| < g
let m be Nat; :: thesis: ( n <= m implies |.(((f2 /* c) . m) - (f2 . x0)).| < g )
assume n <= m ; :: thesis: |.(((f2 /* c) . m) - (f2 . x0)).| < g
A33: m in NAT by ORDINAL1:def 12;
|.(((f2 /* c) . m) - (f2 . x0)).| = |.((f2 . (c . m)) - (f2 . x0)).| by A30, FUNCT_2:108, A33
.= |.((f2 . x0) - (f2 . x0)).| by A21, A33
.= 0 by ABSVALUE:def 1 ;
hence |.(((f2 /* c) . m) - (f2 . x0)).| < g by A32; :: thesis: verum

end;

then A34: f2 /* c is convergent by SEQ_2:def 6;
(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then A35: rng (h + c) c= dom f1 by A19;
then A36: lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = Ldiff (f1,x0) by A1, A16, A18, Th9;
A37: ( h is convergent & (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent ) by A1, A16, A18, A35;
then A38: lim (h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) = (lim h) * (lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) by SEQ_2:15
.= 0 ;
(dom f1) /\ (dom f2) c= dom f2 by XBOOLE_1:17;
then A39: rng (h + c) c= dom f2 by A19;
then A40: lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = Ldiff (f2,x0) by A2, A16, A18, Th9;
A41: (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A16, A18, A35;
then A42: ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c) is convergent by A34;
A43: rng c c= (dom f1) /\ (dom f2) by A24, A30, XBOOLE_1:19;

A44: now :: thesis: for n being Element of NAT holds ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) . n = ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) . n

let n be Element of NAT ; :: thesis: ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) . n = ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) . n
thus ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) . n = ((h ") . n) * ((((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) . n) by SEQ_1:8
.= ((h ") . n) * ((((f1 (#) f2) /* (h + c)) . n) - (((f1 (#) f2) /* c) . n)) by RFUNCT_2:1
.= ((h ") . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 (#) f2) /* c) . n)) by A19, RFUNCT_2:8
.= ((h ") . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 /* c) (#) (f2 /* c)) . n)) by A43, RFUNCT_2:8
.= ((h ") . n) * ((((f1 /* (h + c)) . n) * ((f2 /* (h + c)) . n)) - (((f1 /* c) (#) (f2 /* c)) . n)) by SEQ_1:8
.= ((h ") . n) * ((((f1 /* (h + c)) . n) * ((f2 /* (h + c)) . n)) - (((f1 /* c) . n) * ((f2 /* c) . n))) by SEQ_1:8
.= ((((h ") . n) * (((f2 /* (h + c)) . n) - ((f2 /* c) . n))) * ((f1 /* (h + c)) . n)) + ((((h ") . n) * (((f1 /* (h + c)) . n) - ((f1 /* c) . n))) * ((f2 /* c) . n))
.= ((((h ") . n) * (((f2 /* (h + c)) - (f2 /* c)) . n)) * ((f1 /* (h + c)) . n)) + ((((h ") . n) * (((f1 /* (h + c)) . n) - ((f1 /* c) . n))) * ((f2 /* c) . n)) by RFUNCT_2:1
.= ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) . n) * ((f1 /* (h + c)) . n)) + ((((h ") . n) * (((f1 /* (h + c)) . n) - ((f1 /* c) . n))) * ((f2 /* c) . n)) by SEQ_1:8
.= ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) . n) * ((f1 /* (h + c)) . n)) + ((((h ") . n) * (((f1 /* (h + c)) - (f1 /* c)) . n)) * ((f2 /* c) . n)) by RFUNCT_2:1
.= ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) . n) * ((f1 /* (h + c)) . n)) + ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) by SEQ_1:8
.= ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) . n) + ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) by SEQ_1:8
.= ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) . n) + ((((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) . n) by SEQ_1:8
.= ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) . n by SEQ_1:7 ; :: thesis: verum

end;

then A45: (h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) = (((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) by FUNCT_2:63;

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

let n be Element of NAT ; :: thesis: (h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) . n = ((f1 /* (h + c)) - (f1 /* c)) . n
A46: h . n <> 0 by A18;
thus (h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) . n = ((h (#) (h ")) (#) ((f1 /* (h + c)) - (f1 /* c))) . n by SEQ_1:14
.= ((h (#) (h ")) . n) * (((f1 /* (h + c)) - (f1 /* c)) . n) by SEQ_1:8
.= ((h . n) * ((h ") . n)) * (((f1 /* (h + c)) - (f1 /* c)) . n) by SEQ_1:8
.= ((h . n) * ((h . n) ")) * (((f1 /* (h + c)) - (f1 /* c)) . n) by VALUED_1:10
.= 1 * (((f1 /* (h + c)) - (f1 /* c)) . n) by A46, XCMPLX_0:def 7
.= ((f1 /* (h + c)) - (f1 /* c)) . n ; :: thesis: verum

end;

then A47: h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = (f1 /* (h + c)) - (f1 /* c) by FUNCT_2:63;
h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A37;
then A48: f1 /* (h + c) is convergent by A28, A47, A20;
lim (f1 /* c) = f1 . x0 by A25, A28, SEQ_2:def 7;
then A49: 0 = (lim (f1 /* (h + c))) - (f1 . x0) by A28, A47, A48, A38, SEQ_2:12;
A50: (h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A2, A16, A18, A39;
then A51: ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c)) is convergent by A48;
lim ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = lim ((((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by A44, FUNCT_2:63
.= (lim (((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c)))) + (lim (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by A51, A42, SEQ_2:6
.= ((lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) * (lim (f1 /* (h + c)))) + (lim (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by A50, A48, SEQ_2:15
.= ((lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) * (f1 . x0)) + ((lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) * (lim (f2 /* c))) by A41, A49, A34, SEQ_2:15
.= ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) by A36, A40, A31, A34, SEQ_2:def 7 ;
hence ( (h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) is convergent & lim ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) ) by A51, A42, A45; :: thesis: verum

end;

[.(x0 - (min (r1,r2))),x0.] c= (dom f1) /\ (dom f2) by A14, A11, XBOOLE_1:19;
then [.(x0 - (min (r1,r2))),x0.] c= dom (f1 (#) f2) by VALUED_1:def 4;
hence ( f1 (#) f2 is_left_differentiable_in x0 & Ldiff ((f1 (#) f2),x0) = ((Ldiff (f1,x0)) * (f2 . x0)) + ((Ldiff (f2,x0)) * (f1 . x0)) ) by A7, A15, Th9; :: thesis: verum