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

proof

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

end;

0 <= min r1,r2 by A2, A3, XXREAL_0:15;
then x0 - (min r1,r2) <= x0 by XREAL_1:45;
then A23: x0 in [.(x0 - (min r1,r2)),x0.] by XXREAL_1:1;
then A24: x0 in dom f1 by A12;
A25: rng c c= dom f1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng c ; :: thesis:
hence x in dom f1 by A15, A24, TARSKI:def 1; :: thesis:

end;

A26: for g being real number st 0 < g holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f1 /* c) . m) - (f1 . x0)) < g

proof

let g be real number ; :: thesis:
assume A27: 0 < g ; :: thesis:
take n = 0 ; :: thesis:
let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
abs (((f1 /* c) . m) - (f1 . x0)) = abs ((f1 . (c . m)) - (f1 . x0)) by A25, FUNCT_2:185
.= abs ((f1 . x0) - (f1 . x0)) by A22
.= 0 by ABSVALUE:def 1 ;
hence abs (((f1 /* c) . m) - (f1 . x0)) < g by A27; :: thesis:

end;

A28: ( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
A29: f1 /* c is convergent by A26, SEQ_2:def 6;
then A30: lim (f1 /* c) = f1 . x0 by A26, SEQ_2:def 7;
A31: (h " ) (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A15, A17, A19, Def4;
then A32: h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by A28, SEQ_2:28;
A33: h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) = (f1 /* (h + c)) - (f1 /* c)

proof

now

let n be Element of NAT ; :: thesis:
A34: h . n <> 0 by A17;
thus (h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) . n = ((h (#) (h " )) (#) ((f1 /* (h + c)) - (f1 /* c))) . n by SEQ_1:22
.= ((h (#) (h " )) . n) * (((f1 /* (h + c)) - (f1 /* c)) . n) by SEQ_1:12
.= ((h . n) * ((h " ) . n)) * (((f1 /* (h + c)) - (f1 /* c)) . n) by SEQ_1:12
.= ((h . n) * ((h . n) " )) * (((f1 /* (h + c)) - (f1 /* c)) . n) by VALUED_1:10
.= 1 * (((f1 /* (h + c)) - (f1 /* c)) . n) by A34, XCMPLX_0:def 7
.= ((f1 /* (h + c)) - (f1 /* c)) . n ; :: thesis:

end;

hence h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) = (f1 /* (h + c)) - (f1 /* c) by FUNCT_2:113; :: thesis:

end;

(f1 /* c) + ((f1 /* (h + c)) - (f1 /* c)) = f1 /* (h + c)

proof

now

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

end;

hence (f1 /* c) + ((f1 /* (h + c)) - (f1 /* c)) = f1 /* (h + c) by FUNCT_2:113; :: thesis:

end;

then A35: f1 /* (h + c) is convergent by A29, A32, A33, SEQ_2:19;
lim (h (#) ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) = (lim h) * (lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) by A28, A31, SEQ_2:29
.= 0 by A28 ;
then A36: 0 = (lim (f1 /* (h + c))) - (f1 . x0) by A29, A30, A33, A35, SEQ_2:26;
A37: x0 in dom f2 by A13, A23;
A38: rng c c= dom f2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in rng c ; :: thesis:
hence x in dom f2 by A15, A37, TARSKI:def 1; :: thesis:

end;

A39: for g being real number st 0 < g holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f2 /* c) . m) - (f2 . x0)) < g

proof

let g be real number ; :: thesis:
assume A40: 0 < g ; :: thesis:
take n = 0 ; :: thesis:
let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
abs (((f2 /* c) . m) - (f2 . x0)) = abs ((f2 . (c . m)) - (f2 . x0)) by A38, FUNCT_2:185
.= abs ((f2 . x0) - (f2 . x0)) by A22
.= 0 by ABSVALUE:def 1 ;
hence abs (((f2 /* c) . m) - (f2 . x0)) < g by A40; :: thesis:

end;

then A41: f2 /* c is convergent by SEQ_2:def 6;
A42: rng c c= (dom f1) /\ (dom f2) by A25, A38, XBOOLE_1:19;
A43: ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c)) is convergent by A21, A35, SEQ_2:28;
A44: ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c) is convergent by A20, A41, SEQ_2:28;

A45: now

let n be Element of NAT ; :: thesis:
thus ((h " ) (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) . n = ((h " ) . n) * ((((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) . n) by SEQ_1:12
.= ((h " ) . n) * ((((f1 (#) f2) /* (h + c)) . n) - (((f1 (#) f2) /* c) . n)) by RFUNCT_2:6
.= ((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 (#) f2) /* c) . n)) by A18, RFUNCT_2:23
.= ((h " ) . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 /* c) (#) (f2 /* c)) . n)) by A42, RFUNCT_2:23
.= ((h " ) . n) * ((((f1 /* (h + c)) . n) * ((f2 /* (h + c)) . n)) - (((f1 /* c) (#) (f2 /* c)) . n)) by SEQ_1:12
.= ((h " ) . n) * ((((f1 /* (h + c)) . n) * ((f2 /* (h + c)) . n)) - (((f1 /* c) . n) * ((f2 /* c) . n))) by SEQ_1:12
.= ((((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:6
.= ((((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:12
.= ((((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:6
.= ((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) . n) * ((f1 /* (h + c)) . n)) + ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) by SEQ_1:12
.= ((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) . n) + ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) . n) * ((f2 /* c) . n)) by SEQ_1:12
.= ((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) . n) + ((((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c)) . n) by SEQ_1:12
.= ((((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c))) + (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) . n by SEQ_1:11 ; :: thesis:

end;

then A46: (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:113;
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 A45, FUNCT_2:113
.= (lim (((h " ) (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c)))) + (lim (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by A43, A44, SEQ_2:20
.= ((lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) * (lim (f1 /* (h + c)))) + (lim (((h " ) (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by A21, A35, SEQ_2:29
.= ((lim ((h " ) (#) ((f2 /* (h + c)) - (f2 /* c)))) * (f1 . x0)) + ((lim ((h " ) (#) ((f1 /* (h + c)) - (f1 /* c)))) * (lim (f2 /* c))) by A20, A36, A41, SEQ_2:29
.= ((Ldiff f1,x0) * (f2 . x0)) + ((Ldiff f2,x0) * (f1 . x0)) by A20, A21, A39, A41, 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 A43, A44, A46, SEQ_2:19; :: thesis:

end;

hence ( f1 (#) f2 is_left_differentiable_in x0 & Ldiff (f1 (#) f2),x0 = ((Ldiff f1,x0) * (f2 . x0)) + ((Ldiff f2,x0) * (f1 . x0)) ) by A4, A14, Th9; :: thesis: