let S, T be RealNormSpace; :: thesis: for x0 being Real
for g being PartFunc of REAL, the carrier of S st g is_differentiable_in x0 holds
for f being PartFunc of the carrier of S, the carrier of T 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 Real; :: thesis: for g being PartFunc of REAL, the carrier of S st g is_differentiable_in x0 holds
for f being PartFunc of the carrier of S, the carrier of T 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 g be PartFunc of REAL, the carrier of S; :: thesis: ( g is_differentiable_in x0 implies for f being PartFunc of the carrier of S, the carrier of T 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 the carrier of S, the carrier of T 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 S ex R1 being RestFunc of S 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 the carrier of S, the carrier of T; :: 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 S,T st
( R2 /. (0. S) = 0. T & R2 is_continuous_in 0. S & ( for y being Point of S 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 S,T such that
A6: R2 /. (0. S) = 0. T and
A7: for y being Point of S 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 S,T by LOPBAN_1:def 9;
consider L1 being LinearFunc of S, R1 being RestFunc of S 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 S such that
A9: for p being Real holds L1 /. p = p * r by NDIFF_3:def 2;
reconsider p0 = 0 as Element of REAL by XREAL_0:def 1;
(g /. x0) - (g /. x0) = (L1 /. (x0 - x0)) + (R1 /. (x0 - x0)) by A8, RCOMP_1:16;
then 0. S = (L1 /. 0) + (R1 /. 0) by RLVECT_1:15;
then 0. S = (p0 * r) + (R1 /. 0) by A9;
then 0. S = (0. S) + (R1 /. 0) by RLVECT_1:10;
then R1 /. 0 = 0. S by RLVECT_1:4;
then reconsider R0 = (L2 * R1) + (R2 * (L1 + R1)) as RestFunc of T by A6, Th5;
A10: dom (L2 * L1) = REAL by FUNCT_2:def 1;
reconsider q = L2 . r as Point of T ;
now :: thesis: for pp being Real holds (L2 * L1) /. pp = pp * q
let pp be Real; :: thesis: (L2 * L1) /. pp = pp * q
reconsider p = pp as Element of REAL by XREAL_0:def 1;
L2 . (L1 /. p) = L2 . (p * r) by A9;
then L2 . (L1 /. p) = p * q by LOPBAN_1:def 5;
then (L2 * L1) . p = p * q by A10, FUNCT_1:12;
hence (L2 * L1) /. pp = pp * q by A10, PARTFUN1:def 6; :: thesis: verum
end;
then reconsider L0 = L2 * L1 as LinearFunc of T by NDIFF_3:def 2;
g is_continuous_in x0 by A1, NDIFF_3:22;
then consider N3 being Neighbourhood of x0 such that
A11: g .: N3 c= N2 by NFCONT_3:10;
consider N being Neighbourhood of x0 such that
A12: N c= N1 and
A13: N c= N3 by RCOMP_1:17;
A14: dom L2 = the carrier of S by FUNCT_2:def 1;
then A15: rng R1 c= dom L2 ;
A16: rng L1 c= dom L2 by A14;
now :: thesis: for x being object st x in N holds
x in dom (f * g)
let x be object ; :: thesis: ( x in N implies 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 A12, A17;
then g . x9 in g .: N3 by A2, A13, A17, FUNCT_1:def 6;
then g . x9 in N2 by A11;
hence x in dom (f * g) by A2, A4, A18, FUNCT_1:11; :: thesis: verum
end;
then A19: N c= dom (f * g) ;
A20: 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 A21: x in N ; :: thesis: ((f * g) /. x) - ((f * g) /. x0) = (L0 /. (x - x0)) + (R0 /. (x - x0))
A22: (g /. x) - (g /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A8, A12, A21;
x in N1 by A12, A21;
then g . x in g .: N3 by A2, A13, A21, FUNCT_1:def 6;
then g . x in N2 by A11;
then A24: g /. x in N2 by A2, A12, A21, 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 * R1) = REAL by A26, PARTFUN1:def 2;
L1 + R1 is total by A26, 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 S by PARTFUN1:def 2;
then A30: rng (L1 + R1) c= dom R2 ;
then dom (R2 * (L1 + R1)) = dom (L1 + R1) by RELAT_1:27;
then A31: dom ((L2 * R1) + (R2 * (L1 + R1))) = REAL /\ REAL by A28, A29, VFUNCT_1:def 1;
reconsider dxx0 = x - x0 as Element of REAL by XREAL_0:def 1;
L2 . (R1 /. (x - x0)) = L2 /. (R1 /. (x - x0)) ;
then A32: L2 . (R1 /. (x - x0)) = (L2 * R1) /. dxx0 by A27, A15, PARTFUN2:5;
A33: R2 /. ((L1 /. (x - x0)) + (R1 /. (x - x0))) = R2 /. ((L1 + R1) /. dxx0) by A29, VFUNCT_1:def 1
.= (R2 * (L1 + R1)) /. dxx0 by A29, A30, PARTFUN2:5 ;
A34: dom L1 = REAL by FUNCT_2:def 1;
A35: (L2 * L1) /. (x - x0) = L2 /. (L1 /. dxx0) by PARTFUN2:5, A34, A16;
thus ((f * g) /. x) - ((f * g) /. x0) = (f /. (g /. x)) - ((f * g) /. x0) by A19, A21, PARTFUN2:3
.= (f /. (g /. x)) - (f /. (g /. x0)) by A19, 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 A22, 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 A35, A31, VFUNCT_1:def 1 ; :: thesis: verum
end;
hence A36: f * g is_differentiable_in x0 by A19, NDIFF_3:def 3; :: thesis: diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0))
dom L1 = REAL by FUNCT_2:def 1;
then (L2 * L1) /. 1 = L2 /. (L1 /. jj) by PARTFUN2:5, A16
.= (diff (f,(g /. x0))) . (diff (g,x0)) by A8 ;
hence diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) by A36, A19, A20, NDIFF_3:def 4; :: thesis: verum