let E, F, G be RealNormSpace; :: thesis: for Z being Subset of E
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & v is_differentiable_on T holds
( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) )
let Z be Subset of E; :: thesis: for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & v is_differentiable_on T holds
( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) )
let T be Subset of F; :: thesis: for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & v is_differentiable_on T holds
( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) )
let u be PartFunc of E,F; :: thesis: for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & v is_differentiable_on T holds
( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) )
let v be PartFunc of F,G; :: thesis: ( u .: Z c= T & u is_differentiable_on Z & v is_differentiable_on T implies ( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) ) )
assume that
A1: u .: Z c= T and
A2: u is_differentiable_on Z and
A3: v is_differentiable_on T ; :: thesis: ( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) )
A4: Z is open by A2, NDIFF_1:32;
A5: T is open by A3, NDIFF_1:32;

now :: thesis: for x being object st x in Z holds
x in dom (v * u)

let x be object ; :: thesis: ( x in Z implies x in dom (v * u) )
assume A6: x in Z ; :: thesis: x in dom (v * u)
then u . x in u .: Z by A2, FUNCT_1:def 6;
then u . x in T by A1;
hence x in dom (v * u) by A2, A6, FUNCT_1:11, A3; :: thesis: verum

end;

then A7: Z c= dom (v * u) by TARSKI:def 3;
A8: for x being Point of E st x in Z holds
( v * u is_differentiable_in x & diff ((v * u),x) = (diff (v,(u /. x))) * (diff (u,x)) )

proof

let x be Point of E; :: thesis: ( x in Z implies ( v * u is_differentiable_in x & diff ((v * u),x) = (diff (v,(u /. x))) * (diff (u,x)) ) )
assume A9: x in Z ; :: thesis: ( v * u is_differentiable_in x & diff ((v * u),x) = (diff (v,(u /. x))) * (diff (u,x)) )
then A10: u is_differentiable_in x by A2, A4, NDIFF_1:31;
u /. x in u .: Z by A2, A9, PARTFUN2:23;
then v is_differentiable_in u /. x by A1, A3, A5, NDIFF_1:31;
hence ( v * u is_differentiable_in x & diff ((v * u),x) = (diff (v,(u /. x))) * (diff (u,x)) ) by A10, NDIFF_2:13; :: thesis: verum

end;

then for x being Point of E st x in Z holds
v * u is_differentiable_in x ;
hence A11: v * u is_differentiable_on Z by A4, A7, NDIFF_1:31; :: thesis: for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x)
for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x)

proof

let x be Point of E; :: thesis: ( x in Z implies ((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) )
assume A12: x in Z ; :: thesis: ((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x)
then A13: ((v * u) `| Z) /. x = diff ((v * u),x) by NDIFF_1:def 9, A11
.= (diff (v,(u /. x))) * (diff (u,x)) by A8, A12 ;
u . x in u .: Z by A2, A12, FUNCT_1:def 6;
then u . x in T by A1;
then u /. x in T by A2, A12, PARTFUN1:def 6;
then (diff (v,(u /. x))) * (diff (u,x)) = ((v `| T) /. (u /. x)) * (diff (u,x)) by A3, NDIFF_1:def 9
.= ((v `| T) /. (u /. x)) * ((u `| Z) /. x) by A2, A12, NDIFF_1:def 9 ;
hence ((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) by A13; :: thesis: verum

end;

hence for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ; :: thesis: verum