let n, m be non zero 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 = In (0,REAL) 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 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 A11, PARTFUN1:def 6
.= L2 . (L1 . pp) by A11, A12, FUNCT_1:12
.= 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 (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
A13: 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
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 A14, A17;
then g . x9 in g .: N3 by A2, A15, A17, FUNCT_1:def 6;
then g . x9 in N2 by A13;
hence x in dom (f * g) by A2, A4, A18, FUNCT_1:11; :: 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 A14, A20;
then g . x in g .: N3 by A2, A15, A20, FUNCT_1:def 6;
then A23: g . x in N2 by A13;
x in N1 by A14, A20;
then A24: g /. x in N2 by A2, A23, PARTFUN1:def 6;
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 (REAL-NS n) by FUNCT_2:def 1;
then A29: rng R1 c= dom L2 ;
A30: dom (L2 * R1) = REAL by A26, PARTFUN1:def 2;
A31: L1 + R1 is total by A26, VFUNCT_1:32;
then A32: 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 A33: rng (L1 + R1) c= dom R2 ;
then dom (R2 * (L1 + R1)) = dom (L1 + R1) by RELAT_1:27
.= REAL by A31, PARTFUN1:def 2 ;
then A34: dom ((L2 * R1) + (R2 * (L1 + R1))) = REAL /\ REAL by A30, VFUNCT_1:def 1
.= REAL ;
A35: L2 /. (R1 /. (x - x0)) = L2 /. (R1 /. (x - x0))
.= (L2 * R1) /. (x - x0) by A27, A29, A22, PARTFUN2:5 ;
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 A32, VFUNCT_1:def 1
.= (R2 * (L1 + R1)) /. dxx0 by A32, A33, PARTFUN2:5 ;
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 A37, PARTFUN2:5;
thus ((f * g) /. x) - ((f * g) /. x0) = (f /. (g /. x)) - ((f * g) /. x0) by A16, A20, PARTFUN2:3
.= (f /. (g /. x)) - (f /. (g /. x0)) by A16, A25, PARTFUN2:3
.= ((diff (f,(g /. x0))) . ((g /. x) - (g /. x0))) + (R2 /. ((g /. x) - (g /. x0))) by A7, A24
.= ((L2 /. (L1 /. (x - x0))) + (L2 /. (R1 /. (x - x0)))) + ((R2 * (L1 + R1)) /. (x - x0)) by A21, A36, VECTSP_1:def 20
.= (L2 /. (L1 /. (x - x0))) + (((L2 * R1) /. (x - x0)) + ((R2 * (L1 + R1)) /. (x - x0))) by A35, RLVECT_1:def 3
.= (L0 /. dxx0) + (R0 /. dxx0) by A38, A34, VFUNCT_1:def 1
.= (L0 /. (x - x0)) + (R0 /. (x - x0)) ; :: thesis: verum
end;
hence A39: f * g is_differentiable_in x0 by A16, NDIFF_3:def 3; :: 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 A40, PARTFUN1:def 6
.= L2 . (L1 . jj) by A11, FUNCT_1:12
.= L2 . (L1 /. 1) by A41, PARTFUN1:def 6
.= (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 A39, A16, A42, NDIFF_3:def 4; :: thesis: verum