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) )
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 A2: f2 is_differentiable_in f1 /. x0 ; :: thesis: ( 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
A3: N1 c= dom f1 and
A4: 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;
consider N2 being Neighbourhood of f1 /. x0 such that
A5: N2 c= dom f2 and
A6: 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 A2, NDIFF_1:52;
consider R1 being REST of S,T such that
A7: ( R1 /. (0. S) = 0. T & ( for x being Point of S st x in N1 holds
(f1 /. x) - (f1 /. x0) = ((diff f1,x0) . (x - x0)) + (R1 /. (x - x0)) ) ) by A4;
consider R2 being REST of T,U such that
A8: ( R2 /. (0. T) = 0. U & ( 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 A6;
f1 is_continuous_in x0 by A1, NDIFF_1:49;
then consider N3 being Neighbourhood of x0 such that
A9: f1 .: N3 c= N2 by NFCONT_1:17;
consider N being Neighbourhood of x0 such that
A10: ( N c= N1 & N c= N3 ) by NDIFF_1:1;
A11: 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 A12: x in N ; :: thesis: x in dom (f2 * f1)
then A13: x in N1 by A10;
reconsider x' = x as Point of S by A12;
f1 . x' in f1 .: N3 by A3, A10, A12, A13, FUNCT_1:def 12;
then f1 . x' in N2 by A9;
hence x in dom (f2 * f1) by A3, A5, A13, FUNCT_1:21; :: thesis: verum

end;

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 ;
A14: LB1 = modetrans LB1,S,T by LOPBAN_1:def 12;
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 ;
A15: LB2 = modetrans LB2,T,U by LOPBAN_1:def 12;
set L1 = modetrans (diff f1,x0),S,T;
set L2 = modetrans (diff f2,(f1 /. x0)),T,U;
reconsider R0 = ((modetrans (diff f2,(f1 /. x0)),T,U) * R1) + (R2 * ((modetrans (diff f1,x0),S,T) + R1)) as REST of S,U by A7, A8, Th12;

A16: 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 A17: x in N ; :: thesis: ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (((diff f2,(f1 /. x0)) * (diff f1,x0)) . (x - x0)) + (R0 /. (x - x0))
A18: x in N1 by A10, A17;
A19: (f1 /. x) - (f1 /. x0) = ((diff f1,x0) . (x - x0)) + (R1 /. (x - x0)) by A7, A10, A17;
A20: x0 in N by NFCONT_1:4;
x in N1 by A10, A17;
then f1 . x in f1 .: N3 by A3, A10, A17, FUNCT_1:def 12;
then f1 . x in N2 by A9;
then A21: f1 /. x in N2 by A3, A18, PARTFUN1:def 8;
A22: R1 is total by NDIFF_1:def 5;
then A23: dom R1 = the carrier of S by PARTFUN1:def 4;
R2 is total by NDIFF_1:def 5;
then A24: dom R2 = the carrier of T by PARTFUN1:def 4;
A25: dom (modetrans (diff f1,x0),S,T) = the carrier of S by FUNCT_2:def 1;
A26: (modetrans (diff f1,x0),S,T) + R1 is total by A22, VFUNCT_1:38;
then A27: dom ((modetrans (diff f1,x0),S,T) + R1) = the carrier of S by PARTFUN1:def 4;
A28: rng ((modetrans (diff f1,x0),S,T) + R1) c= dom R2 by A24;
then A29: 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 A26, PARTFUN1:def 4 ;
A30: 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 A27, VFUNCT_1:def 1
.= (R2 * ((modetrans (diff f1,x0),S,T) + R1)) /. (x - x0) by A27, A28, PARTFUN2:10 ;
dom (modetrans (diff f2,(f1 /. x0)),T,U) = the carrier of T by FUNCT_2:def 1;
then A31: rng R1 c= dom (modetrans (diff f2,(f1 /. x0)),T,U) ;
then A32: dom ((modetrans (diff f2,(f1 /. x0)),T,U) * R1) = dom R1 by RELAT_1:46
.= the carrier of S by A22, PARTFUN1:def 4 ;
A33: (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 A23, A31, PARTFUN2:10 ;
A34: 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 A29, A32, VFUNCT_1:def 1
.= the carrier of S ;
A35: (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 A25, FUNCT_1:23;
thus ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (f2 /. (f1 /. x)) - ((f2 * f1) /. x0) by A11, A17, PARTFUN2:6
.= (f2 /. (f1 /. x)) - (f2 /. (f1 /. x0)) by A11, A20, PARTFUN2:6
.= ((diff f2,(f1 /. x0)) . ((f1 /. x) - (f1 /. x0))) + (R2 /. ((f1 /. x) - (f1 /. x0))) by A8, 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 A14, A15, A19, A30, LOPBAN_1:def 5
.= ((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 A33, RLVECT_1:def 6
.= (((diff f2,(f1 /. x0)) * (diff f1,x0)) . (x - x0)) + (R0 /. (x - x0)) by A34, A35, VFUNCT_1:def 1 ; :: thesis: verum

end;

hence f2 * f1 is_differentiable_in x0 by A11, 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 A11, A16, NDIFF_1:def 7; :: thesis: verum