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

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)

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

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

then reconsider L0 = L2 * L1 as LinearFunc of (REAL-NS m) by NDIFF_3:def 2;
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;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

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;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

A19: now :: thesis: for x being Real st x in N holds

((f * g) /. x) - ((f * g) /. x0) = (L0 /. (x - x0)) + (R0 /. (x - x0))

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))((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;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

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