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
( w is_differentiable_on Z & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| 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
( w is_differentiable_on Z & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| 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
( w is_differentiable_on Z & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| 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
( w is_differentiable_on Z & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):> )
let Z be Subset of S; :: thesis: ( w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z implies ( w is_differentiable_on Z & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):> ) )
assume A1: ( w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z ) ; :: thesis: ( w is_differentiable_on Z & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):> )
then A2: ( w is_differentiable_on Z & ( for x being Point of S st x in Z holds
(w `| Z) /. x = <:((u `| Z) /. x),((v `| Z) /. x):> ) ) by Th55;
A3: dom (w `| Z) = Z by A2, NDIFF_1:def 9;
A4: dom (u `| Z) = Z by A1, NDIFF_1:def 9;
A5: dom (v `| Z) = Z by A1, NDIFF_1:def 9;
A6: dom <:(u `| Z),(v `| Z):> = (dom (u `| Z)) /\ (dom (v `| Z)) by FUNCT_3:def 7
.= Z /\ Z by A1, A4, NDIFF_1:def 9
.= Z ;
A7: diff_SP (0,S,E) = E by NDIFF_6:7;
A8: diff_SP (1,S,E) = R_NormSpace_of_BoundedLinearOperators (S,E) by NDIFF_6:7;
A9: diff_SP (0,S,F) = F by NDIFF_6:7;
A10: diff_SP (1,S,F) = R_NormSpace_of_BoundedLinearOperators (S,F) by NDIFF_6:7;
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;
then A11: dom (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) = [#] [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):] by FUNCT_2:def 1;
A12: rng <:(u `| Z),(v `| Z):> c= [:(rng (u `| Z)),(rng (v `| Z)):] by FUNCT_3:51;
[:(rng (u `| Z)),(rng (v `| Z)):] c= [:([#] (diff_SP (1,S,E))),([#] (diff_SP (1,S,F))):] by A8, A10, ZFMISC_1:96;
then A13: dom ((CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):>) = Z by A6, A11, A12, RELAT_1:27, XBOOLE_1:1;
for x0 being object st x0 in dom (w `| Z) holds
(w `| Z) . x0 = ((CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):>) . x0

proof

let x0 be object ; :: thesis: ( x0 in dom (w `| Z) implies (w `| Z) . x0 = ((CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):>) . x0 )
assume A14: x0 in dom (w `| Z) ; :: thesis: (w `| Z) . x0 = ((CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):>) . x0
then reconsider x = x0 as Point of S ;
reconsider f = (u `| Z) /. x as Lipschitzian LinearOperator of S,E by LOPBAN_1:def 9;
reconsider g = (v `| Z) /. x as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
A15: (CTP (S,E,F)) . (f,g) = <:f,g:> by Def3;
A16: (w `| Z) . x0 = (w `| Z) /. x by A14, PARTFUN1:def 6
.= (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) . (((u `| Z) /. x),((v `| Z) /. x)) by A1, A3, A7, A9, A14, A15, Th55
.= (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) . [((u `| Z) /. x),((v `| Z) /. x)] by BINOP_1:def 1
.= (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) . [((u `| Z) . x),((v `| Z) /. x)] by A3, A4, A14, PARTFUN1:def 6
.= (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) . [((u `| Z) . x),((v `| Z) . x)] by A3, A5, A14, PARTFUN1:def 6 ;
[((u `| Z) . x),((v `| Z) . x)] = <:(u `| Z),(v `| Z):> . x by A3, A6, A14, FUNCT_3:def 7;
hence (w `| Z) . x0 = ((CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):>) . x0 by A3, A6, A14, A16, FUNCT_1:13; :: thesis: verum

end;

hence ( w is_differentiable_on Z & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):> ) by A1, A3, A13, Th55, FUNCT_1:2; :: thesis: verum