let S, T be RealNormSpace; :: thesis: for x0 being Point of S
for U being 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 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 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 RestFunc 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:47;
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 RestFunc 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:47;
consider R2 being RestFunc 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 14;
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 14;
then reconsider LB2 = diff (f2,(f1 /. x0)) as Element of BoundedLinearOperators (T,U) ;
consider R1 being RestFunc 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:44;
then consider N3 being Neighbourhood of x0 such that
A10: f1 .: N3 c= N2 by NFCONT_1:10;
reconsider R0 = ((modetrans ((diff (f2,(f1 /. x0))),T,U)) * R1) + (R2 * ((modetrans ((diff (f1,x0)),S,T)) + R1)) as RestFunc 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 object ; :: 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 6;
then f1 . x9 in N2 by A10;
hence x in dom (f2 * f1) by A2, A4, A15, FUNCT_1:11; :: thesis: verum
end;
A16: ( LB1 = modetrans (LB1,S,T) & LB2 = modetrans (LB2,T,U) ) by LOPBAN_1:def 11;
A17: now :: thesis: for x being Point of S st x in N holds
((f2 * f1) /. x) - ((f2 * f1) /. x0) = (((diff (f2,(f1 /. x0))) * (diff (f1,x0))) . (x - x0)) + (R0 /. (x - x0))
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 6;
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 6;
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:13;
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 2;
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:27
.= the carrier of S by A24, PARTFUN1:def 2 ;
A28: (modetrans ((diff (f1,x0)),S,T)) + R1 is total by A24, VFUNCT_1:32;
then A29: dom ((modetrans ((diff (f1,x0)),S,T)) + R1) = the carrier of S by PARTFUN1:def 2;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of T by PARTFUN1:def 2;
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:27
.= the carrier of S by A28, PARTFUN1:def 2 ;
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:5 ;
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:5 ;
thus ((f2 * f1) /. x) - ((f2 * f1) /. x0) = (f2 /. (f1 /. x)) - ((f2 * f1) /. x0) by A13, A18, PARTFUN2:3
.= (f2 /. (f1 /. x)) - (f2 /. (f1 /. x0)) by A13, A23, PARTFUN2:3
.= ((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, VECTSP_1:def 20
.= ((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 3
.= (((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