let S, E, F be RealNormSpace; :: thesis: for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z holds
( diff (w,0,Z) is_differentiable_on Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) st
( T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) & diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) )
let u be PartFunc of S,E; :: thesis: for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z holds
( diff (w,0,Z) is_differentiable_on Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) st
( T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) & diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) )
let v be PartFunc of S,F; :: thesis: for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z holds
( diff (w,0,Z) is_differentiable_on Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) st
( T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) & diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) )
let w be PartFunc of S,[:E,F:]; :: thesis: for Z being Subset of S st w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z holds
( diff (w,0,Z) is_differentiable_on Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) st
( T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) & diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) )
let Z be Subset of S; :: thesis: ( w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z implies ( diff (w,0,Z) is_differentiable_on Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) st
( T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) & diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) ) )
assume A1: ( w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z ) ; :: thesis: ( diff (w,0,Z) is_differentiable_on Z & ex T being Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) st
( T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) & diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> ) )
then A2: ( w is_differentiable_on Z & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):> ) by Th57;
A3: diff (w,1,Z) = (w | Z) `| Z by NDIFF_6:11
.= w `| Z by A1, Th4, Th57 ;
A4: diff (u,1,Z) = (u | Z) `| Z by NDIFF_6:11
.= u `| Z by A1, Th4 ;
A5: diff (v,1,Z) = (v | Z) `| Z by NDIFF_6:11
.= v `| Z by A1, Th4 ;
A6: diff (w,0,Z) = w | Z by NDIFF_6:11;
A7: CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) is Lipschitzian LinearOperator of [:(diff_SP ((0 + 1),S,E)),(diff_SP ((0 + 1),S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (0,S,E)),(diff_SP (0,S,F)):])) by Th56;
A8: diff_SP (0,S,E) = E by NDIFF_6:7;
A9: diff_SP (0,S,F) = F by NDIFF_6:7;
R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (0,S,E)),(diff_SP (0,S,F)):]) = diff_SP (1,S,[:E,F:]) by A8, A9, NDIFF_6:7;
then reconsider T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) as Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) by A7;
diff_SP (0,S,[:E,F:]) = [:E,F:] by NDIFF_6:7;
hence diff (w,0,Z) is_differentiable_on Z by A2, A6, Th3; :: thesis: ex T being Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) st
( T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) & diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> )
take T ; :: thesis: ( T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) & diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> )
thus T = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) ; :: thesis: diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):>
thus diff (w,1,Z) = T * <:(diff (u,1,Z)),(diff (v,1,Z)):> by A1, A3, A4, A5, Th57; :: thesis: verum