let S, T be non trivial RealNormSpace; :: thesis: for x0 being Point of S
for U being non trivial RealNormSpace
for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0) )
let x0 be Point of S; :: thesis: for U being non trivial RealNormSpace
for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0) )
let U be non trivial RealNormSpace; :: thesis: for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0) )
let f1 be PartFunc of S,T; :: thesis: ( f1 is_differentiable_in x0 implies for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0) ) )
assume A1: f1 is_differentiable_in x0 ; :: thesis: for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0) )
consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom f1 and
A3: ex R1 being REST of S,T st
( R1 /. (0. S) = 0. T & R1 is_continuous_in 0. S & ( for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = ((diff f1,x0) . (x - x0)) + (R1 /. (x - x0)) ) ) by A1, NDIFF_1:52;
let f2 be PartFunc of T,U; :: thesis: ( f2 is_differentiable_in f1 /. x0 implies ( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0) ) )
assume f2 is_differentiable_in f1 /. x0 ; :: thesis: ( f2 * f1 is_differentiable_in x0 & diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0) )
then consider N2 being Neighbourhood of f1 /. x0 such that
A4: N2 c= dom f2 and
A5: ex R2 being REST of T,U st
( R2 /. (0. T) = 0. U & R2 is_continuous_in 0. T & ( for y being Point of T st y in N2 holds
(f2 /. y) - (f2 /. (f1 /. x0)) = ((diff f2,(f1 /. x0)) . (y - (f1 /. x0))) + (R2 /. (y - (f1 /. x0))) ) ) by NDIFF_1:52;
consider R2 being REST of T,U such that
A6: R2 /. (0. T) = 0. U and
A7: for y being Point of T st y in N2 holds
(f2 /. y) - (f2 /. (f1 /. x0)) = ((diff f2,(f1 /. x0)) . (y - (f1 /. x0))) + (R2 /. (y - (f1 /. x0))) by A5;
set L2 = modetrans (diff f2,(f1 /. x0)),T,U;
set L1 = modetrans (diff f1,x0),S,T;
R_NormSpace_of_BoundedLinearOperators S,T = NORMSTR(# (BoundedLinearOperators S,T),(Zero_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Add_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Mult_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(BoundedLinearOperatorsNorm S,T) #) by LOPBAN_1:def 15;
then reconsider LB1 = diff f1,x0 as Element of BoundedLinearOperators S,T ;
R_NormSpace_of_BoundedLinearOperators T,U = NORMSTR(# (BoundedLinearOperators T,U),(Zero_ (BoundedLinearOperators T,U),(R_VectorSpace_of_LinearOperators T,U)),(Add_ (BoundedLinearOperators T,U),(R_VectorSpace_of_LinearOperators T,U)),(Mult_ (BoundedLinearOperators T,U),(R_VectorSpace_of_LinearOperators T,U)),(BoundedLinearOperatorsNorm T,U) #) by LOPBAN_1:def 15;
then reconsider LB2 = diff f2,(f1 /. x0) as Element of BoundedLinearOperators T,U ;
consider R1 being REST of S,T such that
A8: R1 /. (0. S) = 0. T and
A9: for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = ((diff f1,x0) . (x - x0)) + (R1 /. (x - x0)) by A3;
f1 is_continuous_in x0 by A1, NDIFF_1:49;
then consider N3 being Neighbourhood of x0 such that
A10: f1 .: N3 c= N2 by NFCONT_1:17;
reconsider R0 = ((modetrans (diff f2,(f1 /. x0)),T,U) * R1) + (R2 * ((modetrans (diff f1,x0),S,T) + R1)) as REST of S,U by A8, A6, Th12;
consider N being Neighbourhood of x0 such that
A11: N c= N1 and
A12: N c= N3 by NDIFF_1:1;
A13: N c= dom (f2 * f1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in N or x in dom (f2 * f1) )
assume A14: x in N ; :: thesis: x in dom (f2 * f1)
then reconsider x9 = x as Point of S ;
A15: x in N1 by A11, A14;
then f1 . x9 in f1 .: N3 by A2, A12, A14, FUNCT_1:def 12;
then f1 . x9 in N2 by A10;
hence x in dom (f2 * f1) by A2, A4, A15, FUNCT_1:21; :: thesis: verum

end;

A16: ( LB1 = modetrans LB1,S,T & LB2 = modetrans LB2,T,U ) by LOPBAN_1:def 12;

A17: now

let x be Point of S; :: thesis: ( x in N implies ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (((diff f2,(f1 /. x0)) * (diff f1,x0)) . (x - x0)) + (R0 /. (x - x0)) )
assume A18: x in N ; :: thesis: ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (((diff f2,(f1 /. x0)) * (diff f1,x0)) . (x - x0)) + (R0 /. (x - x0))
A19: (f1 /. x) - (f1 /. x0) = ((diff f1,x0) . (x - x0)) + (R1 /. (x - x0)) by A9, A11, A18;
x in N1 by A11, A18;
then f1 . x in f1 .: N3 by A2, A12, A18, FUNCT_1:def 12;
then A20: f1 . x in N2 by A10;
x in N1 by A11, A18;
then A21: f1 /. x in N2 by A2, A20, PARTFUN1:def 8;
dom (modetrans (diff f1,x0),S,T) = the carrier of S by FUNCT_2:def 1;
then A22: (modetrans (diff f2,(f1 /. x0)),T,U) . ((modetrans (diff f1,x0),S,T) . (x - x0)) = ((diff f2,(f1 /. x0)) * (diff f1,x0)) . (x - x0) by FUNCT_1:23;
A23: x0 in N by NFCONT_1:4;
A24: R1 is total by NDIFF_1:def 5;
then A25: dom R1 = the carrier of S by PARTFUN1:def 4;
dom (modetrans (diff f2,(f1 /. x0)),T,U) = the carrier of T by FUNCT_2:def 1;
then A26: rng R1 c= dom (modetrans (diff f2,(f1 /. x0)),T,U) ;
then A27: dom ((modetrans (diff f2,(f1 /. x0)),T,U) * R1) = dom R1 by RELAT_1:46
.= the carrier of S by A24, PARTFUN1:def 4 ;
A28: (modetrans (diff f1,x0),S,T) + R1 is total by A24, VFUNCT_1:38;
then A29: dom ((modetrans (diff f1,x0),S,T) + R1) = the carrier of S by PARTFUN1:def 4;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of T by PARTFUN1:def 4;
then A30: rng ((modetrans (diff f1,x0),S,T) + R1) c= dom R2 ;
then dom (R2 * ((modetrans (diff f1,x0),S,T) + R1)) = dom ((modetrans (diff f1,x0),S,T) + R1) by RELAT_1:46
.= the carrier of S by A28, PARTFUN1:def 4 ;
then A31: dom (((modetrans (diff f2,(f1 /. x0)),T,U) * R1) + (R2 * ((modetrans (diff f1,x0),S,T) + R1))) = the carrier of S /\ the carrier of S by A27, VFUNCT_1:def 1
.= the carrier of S ;
A32: (modetrans (diff f2,(f1 /. x0)),T,U) . (R1 /. (x - x0)) = (modetrans (diff f2,(f1 /. x0)),T,U) /. (R1 /. (x - x0))
.= ((modetrans (diff f2,(f1 /. x0)),T,U) * R1) /. (x - x0) by A25, A26, PARTFUN2:10 ;
A33: R2 /. (((modetrans (diff f1,x0),S,T) . (x - x0)) + (R1 /. (x - x0))) = R2 /. (((modetrans (diff f1,x0),S,T) /. (x - x0)) + (R1 /. (x - x0)))
.= R2 /. (((modetrans (diff f1,x0),S,T) + R1) /. (x - x0)) by A29, VFUNCT_1:def 1
.= (R2 * ((modetrans (diff f1,x0),S,T) + R1)) /. (x - x0) by A29, A30, PARTFUN2:10 ;
thus ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (f2 /. (f1 /. x)) - ((f2 * f1) /. x0) by A13, A18, PARTFUN2:6
.= (f2 /. (f1 /. x)) - (f2 /. (f1 /. x0)) by A13, A23, PARTFUN2:6
.= ((diff f2,(f1 /. x0)) . ((f1 /. x) - (f1 /. x0))) + (R2 /. ((f1 /. x) - (f1 /. x0))) by A7, A21
.= (((modetrans (diff f2,(f1 /. x0)),T,U) . ((modetrans (diff f1,x0),S,T) . (x - x0))) + ((modetrans (diff f2,(f1 /. x0)),T,U) . (R1 /. (x - x0)))) + ((R2 * ((modetrans (diff f1,x0),S,T) + R1)) /. (x - x0)) by A16, A19, A33, GRCAT_1:def 13
.= ((modetrans (diff f2,(f1 /. x0)),T,U) . ((modetrans (diff f1,x0),S,T) . (x - x0))) + ((((modetrans (diff f2,(f1 /. x0)),T,U) * R1) /. (x - x0)) + ((R2 * ((modetrans (diff f1,x0),S,T) + R1)) /. (x - x0))) by A32, RLVECT_1:def 6
.= (((diff f2,(f1 /. x0)) * (diff f1,x0)) . (x - x0)) + (R0 /. (x - x0)) by A31, A22, VFUNCT_1:def 1 ; :: thesis: verum

end;

hence f2 * f1 is_differentiable_in x0 by A13, NDIFF_1:def 6; :: thesis: diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0)
hence diff (f2 * f1),x0 = (diff f2,(f1 /. x0)) * (diff f1,x0) by A13, A17, NDIFF_1:def 7; :: thesis: verum