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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng c or x in dom f2 )
assume x in rng c ; :: thesis: x in dom f2
hence x in dom f2 by A17, A22, TARSKI:def 1; :: thesis: verum

end;

A24: 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 A17, TARSKI:def 1; :: thesis: verum

end;

A25: 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: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f2 /* c) . m) - (f2 . x0)) < g )
assume A26: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f2 /* c) . m) - (f2 . x0)) < g
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f2 /* c) . m) - (f2 . x0)) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f2 /* c) . m) - (f2 . x0)) < g )
assume n <= m ; :: thesis: abs (((f2 /* c) . m) - (f2 . x0)) < g
abs (((f2 /* c) . m) - (f2 . x0)) = abs ((f2 . (c . m)) - (f2 . x0)) by A23, FUNCT_2:185
.= abs ((f2 . x0) - (f2 . x0)) by A24
.= 0 by ABSVALUE:def 1 ;
hence abs (((f2 /* c) . m) - (f2 . x0)) < g by A26; :: thesis: verum

end;

then A27: f2 /* c is convergent by SEQ_2:def 6;
(dom f1) /\ (dom f2) c= dom f2 by XBOOLE_1:17;
then A28: rng (h + c) c= dom f2 by A20, XBOOLE_1:1;
then A29: lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) = Rdiff (f2,x0) by A2, A17, A19, Th15;

now

let n be Element of NAT ; :: thesis: (h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) . n = ((f1 /* (h + c)) - (f1 /* c)) . n
A30: h . n <> 0 by A19;
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 A30, XCMPLX_0:def 7
.= ((f1 /* (h + c)) - (f1 /* c)) . n ; :: thesis: verum

end;

then A31: h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = (f1 /* (h + c)) - (f1 /* c) by FUNCT_2:113;
A32: x0 in dom f1 by A14, A21;
A33: 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
hence x in dom f1 by A17, A32, TARSKI:def 1; :: thesis: verum

end;

A34: 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: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f1 /* c) . m) - (f1 . x0)) < g )
assume A35: 0 < g ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f1 /* c) . m) - (f1 . x0)) < g
take n = 0 ; :: thesis: for m being Element of NAT st n <= m holds
abs (((f1 /* c) . m) - (f1 . x0)) < g
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f1 /* c) . m) - (f1 . x0)) < g )
assume n <= m ; :: thesis: abs (((f1 /* c) . m) - (f1 . x0)) < g
abs (((f1 /* c) . m) - (f1 . x0)) = abs ((f1 . (c . m)) - (f1 . x0)) by A33, FUNCT_2:185
.= abs ((f1 . x0) - (f1 . x0)) by A24
.= 0 by ABSVALUE:def 1 ;
hence abs (((f1 /* c) . m) - (f1 . x0)) < g by A35; :: thesis: verum

end;

then A36: f1 /* c is convergent by SEQ_2:def 6;
(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then A37: rng (h + c) c= dom f1 by A20, XBOOLE_1:1;
then A38: lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) = Rdiff (f1,x0) by A1, A17, A19, Th15;
Rdiff (f1,x0) = Rdiff (f1,x0) ;
then A39: (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent by A1, A17, A19, A37, Th15;
then A40: ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c) is convergent by A27, SEQ_2:28;
A41: rng c c= (dom f1) /\ (dom f2) by A33, A23, XBOOLE_1:19;

A42: now

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: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 A20, RFUNCT_2:23
.= ((h ") . n) * ((((f1 /* (h + c)) (#) (f2 /* (h + c))) . n) - (((f1 /* c) (#) (f2 /* c)) . n)) by A41, 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: verum

end;

then A43: (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;

now

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:11
.= ((f1 /* c) . n) + (((f1 /* (h + c)) . n) - ((f1 /* c) . n)) by RFUNCT_2:6
.= (f1 /* (h + c)) . n ; :: thesis: verum

end;

then A44: (f1 /* c) + ((f1 /* (h + c)) - (f1 /* c)) = f1 /* (h + c) by FUNCT_2:113;
A45: lim h = 0 by FDIFF_1:def 1;
A46: ( h is convergent & (h ") (#) ((f1 /* (h + c)) - (f1 /* c)) is convergent ) by A1, A17, A19, A37, Def3, FDIFF_1:def 1;
then h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) is convergent by SEQ_2:28;
then A47: f1 /* (h + c) is convergent by A36, A31, A44, SEQ_2:19;
lim (h (#) ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) = (lim h) * (lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) by A46, SEQ_2:29
.= 0 by A45 ;
then A48: 0 = (lim (f1 /* (h + c))) - (lim (f1 /* c)) by A36, A31, A47, SEQ_2:26
.= (lim (f1 /* (h + c))) - (f1 . x0) by A34, A36, SEQ_2:def 7 ;
Rdiff (f2,x0) = Rdiff (f2,x0) ;
then A49: (h ") (#) ((f2 /* (h + c)) - (f2 /* c)) is convergent by A2, A17, A19, A28, Th15;
then A50: ((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c)) is convergent by A47, SEQ_2:28;
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 A42, FUNCT_2:113
.= (lim (((h ") (#) ((f2 /* (h + c)) - (f2 /* c))) (#) (f1 /* (h + c)))) + (lim (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by A50, A40, SEQ_2:20
.= ((lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) * (lim (f1 /* (h + c)))) + (lim (((h ") (#) ((f1 /* (h + c)) - (f1 /* c))) (#) (f2 /* c))) by A49, A47, SEQ_2:29
.= ((lim ((h ") (#) ((f2 /* (h + c)) - (f2 /* c)))) * (f1 . x0)) + ((lim ((h ") (#) ((f1 /* (h + c)) - (f1 /* c)))) * (lim (f2 /* c))) by A39, A48, A27, SEQ_2:29
.= ((Rdiff (f1,x0)) * (f2 . x0)) + ((Rdiff (f2,x0)) * (f1 . x0)) by A38, A29, A25, A27, SEQ_2:def 7 ;
hence ( (h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c)) is convergent & lim ((h ") (#) (((f1 (#) f2) /* (h + c)) - ((f1 (#) f2) /* c))) = ((Rdiff (f1,x0)) * (f2 . x0)) + ((Rdiff (f2,x0)) * (f1 . x0)) ) by A50, A40, A43, SEQ_2:19; :: thesis: verum

end;

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