let f1, f2 be PartFunc of COMPLEX,COMPLEX; :: thesis:
let x0 be Complex; :: thesis:
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; :: thesis:
consider N2 being Neighbourhood of x0 such that
A3: N2 c= dom f2 and
A4: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2;
consider L2 being C_LinearFunc, R2 being C_RestFunc such that
A5: for x being Complex st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 /. (x - x0)) + (R2 /. (x - x0)) by A4;
reconsider R12 = (f1 /. x0) (#) R2 as C_RestFunc ;
reconsider L12 = (f1 /. x0) (#) L2 as C_LinearFunc ;
consider N1 being Neighbourhood of x0 such that
A6: N1 c= dom f1 and
A7: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1;
consider L1 being C_LinearFunc, R1 being C_RestFunc such that
A8: for x being Complex st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A7;
reconsider R11 = (f2 /. x0) (#) R1 as C_RestFunc ;
reconsider L11 = (f2 /. x0) (#) L1 as C_LinearFunc ;
reconsider R18 = R2 (#) L1 as C_RestFunc ;
reconsider R17 = R1 (#) R2 as C_RestFunc ;
reconsider R16 = R1 (#) L2 as C_RestFunc ;
reconsider R14 = L1 (#) L2 as C_RestFunc ;
reconsider R13 = R11 + R12 as C_RestFunc ;
reconsider L = L11 + L12 as C_LinearFunc ;
reconsider R15 = R13 + R14 as C_RestFunc ;
reconsider R19 = R16 + R17 as C_RestFunc ;
reconsider R20 = R19 + R18 as C_RestFunc ;
reconsider R = R15 + R20 as C_RestFunc ;
consider N being Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Lm1;
A11: N c= dom f2 by A3, A10;
N c= dom f1 by A6, A9;
then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27;
then A12: N c= dom (f1 (#) f2) by VALUED_1:def 4;

A13: now :: thesis:

let x be Complex; :: thesis:
A14: x0 in N by Th7;
A15: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume A16: x in N ; :: thesis:
then A17: ((f1 /. x) - (f1 /. x0)) + (f1 /. x0) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0) by A8, A9;
thus ((f1 (#) f2) /. x) - ((f1 (#) f2) /. x0) = ((f1 /. x) * (f2 /. x)) - ((f1 (#) f2) /. x0) by A12, A16, CFUNCT_1:3
.= ((((f1 /. x) * (f2 /. x)) + (- ((f1 /. x) * (f2 /. x0)))) + ((f1 /. x) * (f2 /. x0))) - ((f1 /. x0) * (f2 /. x0)) by A12, A14, CFUNCT_1:3
.= ((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 A8, A9, A16
.= ((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 CFUNCT_1:65, A15
.= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) * ((f2 /. x) - (f2 /. x0))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by A17, CFUNCT_1:65, A15
.= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by A5, A10, A16
.= ((((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 CFUNCT_1:65, A15
.= ((((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 CFUNCT_1:65, A15
.= (((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 CFUNCT_1:64, A15
.= (((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 CFUNCT_1:64, A15
.= (((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 CFUNCT_1:64, A15
.= (((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 CFUNCT_1:64, A15
.= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + ((R16 /. (x - x0)) + ((R1 /. (x - x0)) * (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64, A15
.= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + ((R16 /. (x - x0)) + (R17 /. (x - x0)))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64, A15
.= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + (R19 /. (x - x0))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64, A15
.= ((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 CFUNCT_1:64, A15
.= (L /. (x - x0)) + (((R13 /. (x - x0)) + (R14 /. (x - x0))) + (R20 /. (x - x0)))
.= (L /. (x - x0)) + ((R15 /. (x - x0)) + (R20 /. (x - x0))) by CFUNCT_1:64, A15
.= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:64, A15 ; :: thesis:

end;

hence f1 (#) f2 is_differentiable_in x0 by A12; :: thesis:
hence diff ((f1 (#) f2),x0) = L /. 1r by A12, A13, Def7
.= (L11 /. 1r) + (L12 /. 1r) by CFUNCT_1:64
.= ((f2 /. x0) * (L1 /. 1r)) + (L12 /. 1r) by CFUNCT_1:65
.= ((f2 /. x0) * (L1 /. 1r)) + ((f1 /. x0) * (L2 /. 1r)) by CFUNCT_1:65
.= ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (L2 /. 1r)) by A1, A6, A8, Def7
.= ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) by A2, A3, A5, Def7 ;
:: thesis: