let n, m be non empty Element of NAT ; :: thesis: for x0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds
for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
let x0 be Element of REAL ; :: thesis: for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds
for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
set S = REAL-NS n;
set T = REAL-NS m;
let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( g is_differentiable_in x0 implies for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) )
assume A1: g is_differentiable_in x0 ; :: thesis: for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom g and
A3: ex L1 being LinearFunc of (REAL-NS n) ex R1 being RestFunc of (REAL-NS n) st
( diff (g,x0) = L1 . 1 & ( for x being Real st x in N1 holds
(g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) ) ) by A1, NDIFF_3:def 4;
let f be PartFunc of (REAL-NS n),(REAL-NS m); :: thesis: ( f is_differentiable_in g /. x0 implies ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) ) )
assume f is_differentiable_in g /. x0 ; :: thesis: ( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )
then consider N2 being Neighbourhood of g /. x0 such that
A4: N2 c= dom f and
A5: ex R2 being RestFunc of (REAL-NS n),(REAL-NS m) st
( R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) & R2 is_continuous_in 0. (REAL-NS n) & ( for y being Point of (REAL-NS n) st y in N2 holds
(f /. y) - (f /. (g /. x0)) = ((diff (f,(g /. x0))) . (y - (g /. x0))) + (R2 /. (y - (g /. x0))) ) ) by NDIFF_1:47;
consider R2 being RestFunc of (REAL-NS n),(REAL-NS m) such that
A6: R2 /. (0. (REAL-NS n)) = 0. (REAL-NS m) and
A7: for y being Point of (REAL-NS n) st y in N2 holds
(f /. y) - (f /. (g /. x0)) = ((diff (f,(g /. x0))) . (y - (g /. x0))) + (R2 /. (y - (g /. x0))) by A5;
reconsider L2 = diff (f,(g /. x0)) as Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS m) by LOPBAN_1:def 9;
consider L1 being LinearFunc of (REAL-NS n), R1 being RestFunc of (REAL-NS n) such that
A8: ( diff (g,x0) = L1 . 1 & ( for x being Real st x in N1 holds
(g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) ) ) by A3;
consider r being Point of (REAL-NS n) such that
A9: for p being Real holds L1 . p = p * r by NDIFF_3:def 2;
reconsider p0 = 0 as Element of REAL ;
(g /. x0) - (g /. x0) = (L1 . (x0 - x0)) + (R1 /. (x0 - x0)) by A8, RCOMP_1:16;
then 0. (REAL-NS n) = (L1 . 0) + (R1 /. 0) by RLVECT_1:15;
then 0. (REAL-NS n) = (p0 * r) + (R1 /. 0) by A9;
then 0. (REAL-NS n) = (0. (REAL-NS n)) + (R1 /. 0) by RLVECT_1:10;
then A10: R1 /. 0 = 0. (REAL-NS n) by RLVECT_1:4;
A11: dom (L2 * L1) = REAL by FUNCT_2:def 1;
reconsider q = L2 . r as Point of (REAL-NS m) ;
for p being Real holds (L2 * L1) . p = p * q

proof

let p be Real; :: thesis: (L2 * L1) . p = p * q
L2 . (L1 . p) = L2 . (p * r) by A9
.= p * q by LOPBAN_1:def 5 ;
hence (L2 * L1) . p = p * q by A11, FUNCT_1:12; :: thesis: verum

end;

then reconsider L0 = L2 * L1 as LinearFunc of (REAL-NS m) by NDIFF_3:def 2;
g is_continuous_in x0 by A1, NDIFF_3:22;
then consider N3 being Neighbourhood of x0 such that
A12: g .: N3 c= N2 by NFCONT_3:10;
reconsider R0 = (L2 * R1) + (R2 * (L1 + R1)) as RestFunc of (REAL-NS m) by A10, A6, Th49;
consider N being Neighbourhood of x0 such that
A13: N c= N1 and
A14: N c= N3 by RCOMP_1:17;
A15: N c= dom (f * g)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in dom (f * g) )
assume A16: x in N ; :: thesis: x in dom (f * g)
then reconsider x9 = x as Real ;
A17: x in N1 by A13, A16;
then g . x9 in g .: N3 by A2, A14, A16, FUNCT_1:def 6;
then g . x9 in N2 by A12;
hence x in dom (f * g) by A2, A4, A17, FUNCT_1:11; :: thesis: verum

end;

A18: now :: thesis: for x being Real st x in N holds
((f * g) /. x) - ((f * g) /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0))

let x be Real; :: thesis: ( x in N implies ((f * g) /. x) - ((f * g) /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0)) )
assume A19: x in N ; :: thesis: ((f * g) /. x) - ((f * g) /. x0) = (L0 . (x - x0)) + (R0 /. (x - x0))
A20: (g /. x) - (g /. x0) = (L1 . (x - x0)) + (R1 /. (x - x0)) by A8, A13, A19;
x in N1 by A13, A19;
then g . x in g .: N3 by A2, A14, A19, FUNCT_1:def 6;
then A21: g . x in N2 by A12;
x in N1 by A13, A19;
then A22: g /. x in N2 by A2, A21, PARTFUN1:def 6;
A23: x0 in N by RCOMP_1:16;
A24: R1 is total by NDIFF_3:def 1;
then A25: dom R1 = REAL by PARTFUN1:def 2;
dom L2 = the carrier of (REAL-NS n) by FUNCT_2:def 1;
then A26: rng R1 c= dom L2 ;
A27: dom (L2 * R1) = REAL by A24, PARTFUN1:def 2;
A28: L1 + R1 is total by A24, VFUNCT_1:32;
then A29: dom (L1 + R1) = REAL by PARTFUN1:def 2;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of (REAL-NS n) by PARTFUN1:def 2;
then A30: rng (L1 + R1) c= dom R2 ;
then dom (R2 * (L1 + R1)) = dom (L1 + R1) by RELAT_1:27
.= REAL by A28, PARTFUN1:def 2 ;
then A31: dom ((L2 * R1) + (R2 * (L1 + R1))) = REAL /\ REAL by A27, VFUNCT_1:def 1
.= REAL ;
A32: L2 . (R1 /. (x - x0)) = L2 /. (R1 /. (x - x0))
.= (L2 * R1) /. (x - x0) by A25, A26, PARTFUN2:5 ;
A33: R2 /. ((L1 . (x - x0)) + (R1 /. (x - x0))) = R2 /. ((L1 /. (x - x0)) + (R1 /. (x - x0)))
.= R2 /. ((L1 + R1) /. (x - x0)) by A29, VFUNCT_1:def 1
.= (R2 * (L1 + R1)) /. (x - x0) by A29, A30, PARTFUN2:5 ;
A34: (L2 * L1) . (x - x0) = L2 . (L1 . (x - x0)) by A11, FUNCT_1:12;
thus ((f * g) /. x) - ((f * g) /. x0) = (f /. (g /. x)) - ((f * g) /. x0) by A15, A19, PARTFUN2:3
.= (f /. (g /. x)) - (f /. (g /. x0)) by A15, A23, PARTFUN2:3
.= ((diff (f,(g /. x0))) . ((g /. x) - (g /. x0))) + (R2 /. ((g /. x) - (g /. x0))) by A7, A22
.= ((L2 . (L1 . (x - x0))) + (L2 . (R1 /. (x - x0)))) + ((R2 * (L1 + R1)) /. (x - x0)) by A20, A33, VECTSP_1:def 20
.= (L2 . (L1 . (x - x0))) + (((L2 * R1) /. (x - x0)) + ((R2 * (L1 + R1)) /. (x - x0))) by A32, RLVECT_1:def 3
.= (L0 . (x - x0)) + (R0 /. (x - x0)) by A34, A31, VFUNCT_1:def 1 ; :: thesis: verum

end;

hence A35: f * g is_differentiable_in x0 by A15, NDIFF_3:def 3; :: thesis: diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0))
(L2 * L1) . 1 = (diff (f,(g /. x0))) . (diff (g,x0)) by A8, A11, FUNCT_1:12;
hence diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) by A35, A15, A18, NDIFF_3:def 4; :: thesis: verum