let n, m be non zero Element of NAT ; :: thesis: for x0 being Element of REAL
for g being PartFunc of REAL,() st g is_differentiable_in x0 holds
for f being PartFunc of (),() 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,() st g is_differentiable_in x0 holds
for f being PartFunc of (),() 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,(); :: thesis: ( g is_differentiable_in x0 implies for f being PartFunc of (),() 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 (),() 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 () ex R1 being RestFunc of () 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 ;
let f be PartFunc of (),(); :: 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 (),() st
( R2 /. (0. ()) = 0. () & R2 is_continuous_in 0. () & ( for y being Point of () 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 (),() such that
A6: R2 /. (0. ()) = 0. () and
A7: for y being Point of () 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 (),() by LOPBAN_1:def 9;
consider L1 being LinearFunc of (), R1 being RestFunc of () 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 () such that
A9: for p being Real holds L1 /. p = p * r by NDIFF_3:def 2;
reconsider p0 = In (0,REAL) as Element of REAL ;
(g /. x0) - (g /. x0) = (L1 /. (x0 - x0)) + (R1 /. (x0 - x0)) by ;
then 0. () = (L1 /. 0) + (R1 /. 0) by RLVECT_1:15;
then 0. () = (p0 * r) + (R1 /. 0) by A9;
then 0. () = (0. ()) + (R1 /. 0) by RLVECT_1:10;
then A10: R1 /. 0 = 0. () by RLVECT_1:4;
A11: dom (L2 * L1) = REAL by FUNCT_2:def 1;
reconsider q = L2 . r as Point of () ;
for p being Real holds (L2 * L1) /. p = p * q
proof
let pp be Real; :: thesis: (L2 * L1) /. pp = pp * q
reconsider p = pp as Element of REAL by XREAL_0:def 1;
A12: pp in REAL by XREAL_0:def 1;
hence (L2 * L1) /. pp = (L2 * L1) . pp by
.= L2 . (L1 . pp) by
.= L2 . (L1 /. p)
.= L2 . (p * r) by A9
.= pp * q by LOPBAN_1:def 5 ;
:: thesis: verum
end;
then reconsider L0 = L2 * L1 as LinearFunc of () by NDIFF_3:def 2;
g is_continuous_in x0 by ;
then consider N3 being Neighbourhood of x0 such that
A13: g .: N3 c= N2 by NFCONT_3:10;
reconsider R0 = (L2 * R1) + (R2 * (L1 + R1)) as RestFunc of () by ;
consider N being Neighbourhood of x0 such that
A14: N c= N1 and
A15: N c= N3 by RCOMP_1:17;
A16: N c= dom (f * g)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in dom (f * g) )
assume A17: x in N ; :: thesis: x in dom (f * g)
then reconsider x9 = x as Real ;
A18: x in N1 by ;
then g . x9 in g .: N3 by ;
then g . x9 in N2 by A13;
hence x in dom (f * g) by ; :: thesis: verum
end;
A19: 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 A20: x in N ; :: thesis: ((f * g) /. x) - ((f * g) /. x0) = (L0 /. (x - x0)) + (R0 /. (x - x0))
A21: (g /. x) - (g /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A8, A14, A20;
A22: x - x0 in REAL by XREAL_0:def 1;
x in N1 by ;
then g . x in g .: N3 by ;
then A23: g . x in N2 by A13;
x in N1 by ;
then A24: g /. x in N2 by ;
A25: x0 in N by RCOMP_1:16;
A26: R1 is total by NDIFF_3:def 1;
then A27: dom R1 = REAL by PARTFUN1:def 2;
A28: dom L2 = the carrier of () by FUNCT_2:def 1;
then A29: rng R1 c= dom L2 ;
A30: dom (L2 * R1) = REAL by ;
A31: L1 + R1 is total by ;
then A32: dom (L1 + R1) = REAL by PARTFUN1:def 2;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of () by PARTFUN1:def 2;
then A33: rng (L1 + R1) c= dom R2 ;
then dom (R2 * (L1 + R1)) = dom (L1 + R1) by RELAT_1:27
.= REAL by ;
then A34: dom ((L2 * R1) + (R2 * (L1 + R1))) = REAL /\ REAL by
.= REAL ;
A35: L2 /. (R1 /. (x - x0)) = L2 /. (R1 /. (x - x0))
.= (L2 * R1) /. (x - x0) by ;
reconsider dxx0 = x - x0 as Element of REAL by XREAL_0:def 1;
A36: R2 /. ((L1 /. (x - x0)) + (R1 /. (x - x0))) = R2 /. ((L1 /. (x - x0)) + (R1 /. (x - x0)))
.= R2 /. ((L1 + R1) /. dxx0) by
.= (R2 * (L1 + R1)) /. dxx0 by ;
A37: dom L1 = REAL by FUNCT_2:def 1;
rng L1 c= dom L2 by A28;
then A38: (L2 * L1) /. dxx0 = L2 /. (L1 /. dxx0) by ;
thus ((f * g) /. x) - ((f * g) /. x0) = (f /. (g /. x)) - ((f * g) /. x0) by
.= (f /. (g /. x)) - (f /. (g /. x0)) by
.= ((diff (f,(g /. x0))) . ((g /. x) - (g /. x0))) + (R2 /. ((g /. x) - (g /. x0))) by
.= ((L2 /. (L1 /. (x - x0))) + (L2 /. (R1 /. (x - x0)))) + ((R2 * (L1 + R1)) /. (x - x0)) by
.= (L2 /. (L1 /. (x - x0))) + (((L2 * R1) /. (x - x0)) + ((R2 * (L1 + R1)) /. (x - x0))) by
.= (L0 /. dxx0) + (R0 /. dxx0) by
.= (L0 /. (x - x0)) + (R0 /. (x - x0)) ; :: thesis: verum
end;
hence A39: f * g is_differentiable_in x0 by ; :: thesis: diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0))
A40: jj in dom L0 by A11;
dom L1 = REAL by FUNCT_2:def 1;
then A41: jj in dom L1 ;
A42: L0 /. 1 = L0 . 1 by
.= L2 . (L1 . jj) by
.= L2 . (L1 /. 1) by
.= (diff (f,(g /. x0))) . (diff (g,x0)) by A8 ;
for x being Real st x in N holds
((f * g) /. x) - ((f * g) /. x0) = (L0 /. (x - x0)) + (R0 /. (x - x0)) by A19;
hence diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) by ; :: thesis: verum