let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) )
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) ) )
reconsider j = 1 as Element of REAL by XREAL_0:def 1;
assume that
A1:
f1 is_differentiable_in x0
and
A2:
f2 is_differentiable_in x0
; ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0))) )
consider N1 being Neighbourhood of x0 such that
A3:
N1 c= dom f1
and
A4:
ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N1 holds
(f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0))
by A1;
consider L1 being LinearFunc, R1 being RestFunc 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 LinearFunc ex R being RestFunc st
for x being Real st x in N2 holds
(f2 . x) - (f2 . x0) = (L . (x - x0)) + (R . (x - x0))
by A2;
consider L2 being LinearFunc, R2 being RestFunc 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 RestFunc by Th7;
reconsider R17 = R1 (#) R2 as RestFunc by Th4;
A9:
R18 is total
by Def2;
reconsider R16 = R1 (#) L2 as RestFunc by Th7;
reconsider R14 = L1 (#) L2 as RestFunc by Th6;
reconsider R19 = R16 + R17 as RestFunc by Th4;
reconsider R20 = R19 + R18 as RestFunc by Th4;
A10:
R14 is total
by Def2;
reconsider R12 = (f1 . x0) (#) R2 as RestFunc by Th5;
A11:
R2 is total
by Def2;
reconsider L11 = (f2 . x0) (#) L1 as LinearFunc by Th3;
A12:
L1 is total
by Def3;
reconsider R11 = (f2 . x0) (#) R1 as RestFunc by Th5;
A13:
R1 is total
by Def2;
reconsider R13 = R11 + R12 as RestFunc by Th4;
reconsider R15 = R13 + R14 as RestFunc by Th4;
reconsider R = R15 + R20 as RestFunc by Th4;
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;
N c= dom f1
by A3, A14;
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 LinearFunc by Th3;
A18:
L2 is total
by Def3;
reconsider L = L11 + L12 as LinearFunc by Th2;
A19:
R16 is total
by Def2;
A20:
( L11 is total & L12 is total )
by Def3;
A21:
now for x being Real st x in N holds
((f1 (#) f2) . x) - ((f1 (#) f2) . x0) = (L . (x - x0)) + (R . (x - x0))let x be
Real;
( x in N implies ((f1 (#) f2) . x) - ((f1 (#) f2) . x0) = (L . (x - x0)) + (R . (x - x0)) )reconsider xx =
x,
xx0 =
x0,
xxx0 =
x - x0 as
Element of
REAL by XREAL_0:def 1;
assume A22:
x in N
;
((f1 (#) f2) . x) - ((f1 (#) f2) . x0) = (L . (x - x0)) + (R . (x - x0))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 . xx) * ((f2 . xx) - (f2 . xx0))) + ((L11 . (xx - xx0)) + ((f2 . xx0) * (R1 . (xx - xx0))))
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 . (xx - xx0)) + (R1 . (xx - xx0))) * ((L2 . (xx - xx0)) + (R2 . (xx - xx0)))) + ((L12 . (xx - x0)) + ((f1 . x0) * (R2 . (xx - x0))))) + ((L11 . (xx - x0)) + (R11 . (xx - 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 . (xx - x0)) + (R1 . (xx - x0))) * ((L2 . (xx - x0)) + (R2 . (xx - x0)))) + ((L12 . (xx - x0)) + ((L11 . (xx - x0)) + (R13 . (xx - xx0))))
by A13, A11, RFUNCT_1:56
.=
(((L1 . (xx - x0)) + (R1 . (xx - x0))) * ((L2 . (xx - x0)) + (R2 . (xx - x0)))) + (((L11 . (xx - x0)) + (L12 . (xx - x0))) + (R13 . (xx - xx0)))
.=
((((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 . (xx - x0)) + ((R2 . (x - x0)) * (L1 . (x - x0)))) + ((R1 . (x - x0)) * ((L2 . (x - x0)) + (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . xxx0))
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 . (xx - xx0)))
by A12, A11, RFUNCT_1:56
.=
(((R14 . (xx - x0)) + (R18 . (x - x0))) + ((R16 . (x - x0)) + ((R1 . (x - x0)) * (R2 . (x - x0))))) + ((L . (x - x0)) + (R13 . xxx0))
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 . (xx - xx0)) + (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 . xxx0) + (R13 . (x - xx0))) + ((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 . (xx - xx0)) + ((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
;
verum end;
hence
f1 (#) f2 is_differentiable_in x0
by A17; diff ((f1 (#) f2),x0) = ((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0)))
hence diff ((f1 (#) f2),x0) =
L . 1
by A17, A21, Def5
.=
(L11 . j) + (L12 . j)
by A20, RFUNCT_1:56
.=
((f2 . x0) * (L1 . j)) + (L12 . j)
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, Def5
.=
((f2 . x0) * (diff (f1,x0))) + ((f1 . x0) * (diff (f2,x0)))
by A2, A6, A8, Def5
;
verum