let x0 be Real; :: thesis:
let f1, f2 be PartFunc of REAL,REAL; :: thesis:
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; :: thesis:
consider N1 being Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L being LINEAR ex R being REST st
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) by A1, Def5;
consider L1 being LINEAR, R1 being REST such that
A5: for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A4;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L being LINEAR ex R being REST st
for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0)) by A2, Def5;
consider L2 being LINEAR, R2 being REST such that
A8: for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L2 . (x - x0)) + (R2 . (x - x0)) by A7;
reconsider R18 = R2 (#) L1 as REST by Th11;
reconsider R17 = R1 (#) R2 as REST by Th8;
A9: R18 is total by Def3;
reconsider R16 = R1 (#) L2 as REST by Th11;
reconsider R14 = L1 (#) L2 as REST by Th10;
reconsider R19 = R16 + R17 as REST by Th8;
reconsider R20 = R19 + R18 as REST by Th8;
A10: R14 is total by Def3;
reconsider R12 = (f1 . x0) (#) R2 as REST by Th9;
A11: R2 is total by Def3;
reconsider L11 = (f2 . x0) (#) L1 as LINEAR by Th7;
A12: L1 is total by Def4;
reconsider R11 = (f2 . x0) (#) R1 as REST by Th9;
A13: R1 is total by Def3;
reconsider R13 = R11 + R12 as REST by Th8;
reconsider R15 = R13 + R14 as REST by Th8;
reconsider R = R15 + R20 as REST by Th8;
consider N being Neighbourhood of x0 such that
A14: N c= N1 and
A15: N c= N2 by RCOMP_1:17;
A16: N c= dom f2 by A6, A15, XBOOLE_1:1;
N c= dom f1 by A3, A14, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A16, XBOOLE_1:27;
then A17: N c= dom (f1 (#) f2) by VALUED_1:def 4;
reconsider L12 = (f1 . x0) (#) L2 as LINEAR by Th7;
A18: L2 is total by Def4;
reconsider L = L11 + L12 as LINEAR by Th6;
A19: R16 is total by Def3;
A20: ( L11 is total & L12 is total ) by Def4;

A21: now

let x be Real; :: thesis:
assume A22: x in N ; :: thesis:
then A23: ((f1 . x) - (f1 . x0)) + (f1 . x0) = ((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0) by A5, A14;
thus ((f1 (#) f2) . x) - ((f1 (#) f2) . x0) = ((f1 . x) * (f2 . x)) - ((f1 (#) f2) . x0) by VALUED_1:5
.= ((((f1 . x) * (f2 . x)) + (- ((f1 . x) * (f2 . x0)))) + ((f1 . x) * (f2 . x0))) - ((f1 . x0) * (f2 . x0)) by VALUED_1:5
.= ((f1 . x) * ((f2 . x) - (f2 . x0))) + (((f1 . x) - (f1 . x0)) * (f2 . x0))
.= ((f1 . x) * ((f2 . x) - (f2 . x0))) + (((L1 . (x - x0)) + (R1 . (x - x0))) * (f2 . x0)) by A5, A14, A22
.= ((f1 . x) * ((f2 . x) - (f2 . x0))) + (((f2 . x0) * (L1 . (x - x0))) + ((R1 . (x - x0)) * (f2 . x0)))
.= ((f1 . x) * ((f2 . x) - (f2 . x0))) + ((L11 . (x - x0)) + ((f2 . x0) * (R1 . (x - x0)))) by A12, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0)) * ((f2 . x) - (f2 . x0))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A13, A23, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) + (f1 . x0)) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A8, A15, A22
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + (((f1 . x0) * (L2 . (x - x0))) + ((f1 . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0)))
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((f1 . x0) * (R2 . (x - x0))))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A18, RFUNCT_1:57
.= ((((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + (R12 . (x - x0)))) + ((L11 . (x - x0)) + (R11 . (x - x0))) by A11, RFUNCT_1:57
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + ((R11 . (x - x0)) + (R12 . (x - x0)))))
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + ((L12 . (x - x0)) + ((L11 . (x - x0)) + (R13 . (x - x0)))) by A13, A11, RFUNCT_1:56
.= (((L1 . (x - x0)) + (R1 . (x - x0))) * ((L2 . (x - x0)) + (R2 . (x - x0)))) + (((L11 . (x - x0)) + (L12 . (x - x0))) + (R13 . (x - x0)))
.= ((((L1 . (x - x0)) * (L2 . (x - x0))) + ((L1 . (x - x0)) * (R2 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A20, RFUNCT_1:56
.= (((R14 . (x - x0)) + ((R2 . (x - x0)) * (L1 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A12, A18, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + (((R1 . (x - x0)) * (L2 . (x - x0))) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A12, A11, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . (x - x0))) by A18, A13, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + (R17 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0))) by A13, A11, RFUNCT_1:56
.= (((R14 . (x - x0)) + (R18 . (x - x0))) + (R19 . (x - x0))) + ((L . (x - x0)) + (R13 . (x - x0))) by A13, A11, A19, RFUNCT_1:56
.= ((R14 . (x - x0)) + ((R19 . (x - x0)) + (R18 . (x - x0)))) + ((L . (x - x0)) + (R13 . (x - x0)))
.= ((L . (x - x0)) + (R13 . (x - x0))) + ((R14 . (x - x0)) + (R20 . (x - x0))) by A13, A11, A19, A9, RFUNCT_1:56
.= (L . (x - x0)) + (((R13 . (x - x0)) + (R14 . (x - x0))) + (R20 . (x - x0)))
.= (L . (x - x0)) + ((R15 . (x - x0)) + (R20 . (x - x0))) by A13, A11, A10, RFUNCT_1:56
.= (L . (x - x0)) + (R . (x - x0)) by A13, A11, A10, A19, A9, RFUNCT_1:56 ; :: thesis:

end;

hence f1 (#) f2 is_differentiable_in x0 by A17, Def5; :: thesis:
hence diff ((f1 (#) f2),x0) = L . 1 by A17, A21, Def6
.= (L11 . 1) + (L12 . 1) by A20, RFUNCT_1:56
.= ((f2 . x0) * (L1 . 1)) + (L12 . 1) by A12, RFUNCT_1:57
.= ((f2 . x0) * (L1 . 1)) + ((f1 . x0) * (L2 . 1)) by A18, RFUNCT_1:57
.= ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (L2 . 1)) by A1, A3, A5, Def6
.= ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) by A2, A6, A8, Def6 ;
:: thesis: