let S, E, F be RealNormSpace; :: thesis:
let u be PartFunc of S,E; :: thesis:
let v be PartFunc of S,F; :: thesis:
let w be PartFunc of S,[:E,F:]; :: thesis:
let Z be Subset of S; :: thesis:
assume A1: ( w = <:u,v:> & u is_differentiable_on 2,Z & v is_differentiable_on 2,Z ) ; :: thesis:
then A2: ( u is_differentiable_on 1,Z & v is_differentiable_on 1,Z ) by NDIFF_6:17;
then A3: ( u | Z is_differentiable_on Z & v | Z is_differentiable_on Z ) by NDIFF_6:15;
( u is_differentiable_on Z & v is_differentiable_on Z ) by A2, Th3, NDIFF_6:15;
then A4: ( 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)):> ) ) by A1, Th58;
A5: diff_SP (0,S,[:E,F:]) = [:E,F:] by NDIFF_6:7;
A6: diff (w,0,Z) = w | Z by NDIFF_6:11;
A7: w | Z is_differentiable_on Z by A4, A5, NDIFF_6:11;
A8: w is_differentiable_on Z by A4, A5, A6, Th3;
set E1 = diff_SP (1,S,E);
set F1 = diff_SP (1,S,F);
set u1 = diff (u,1,Z);
set v1 = diff (v,1,Z);
set w1 = <:(diff (u,1,Z)),(diff (v,1,Z)):>;
diff (u,1,Z) = (u | Z) `| Z by NDIFF_6:11;
then A9: dom (diff (u,1,Z)) = Z by A3, NDIFF_1:def 9;
diff (v,1,Z) = (v | Z) `| Z by NDIFF_6:11;
then A10: dom (diff (v,1,Z)) = Z by A3, NDIFF_1:def 9;
A11: dom <:(diff (u,1,Z)),(diff (v,1,Z)):> = (dom (diff (u,1,Z))) /\ (dom (diff (v,1,Z))) by FUNCT_3:def 7
.= Z by A9, A10 ;
A12: [:(rng (diff (u,1,Z))),(rng (diff (v,1,Z))):] c= [#] [:([#] (diff_SP (1,S,E))),([#] (diff_SP (1,S,F))):] by ZFMISC_1:96;
rng <:(diff (u,1,Z)),(diff (v,1,Z)):> c= [:(rng (diff (u,1,Z))),(rng (diff (v,1,Z))):] by FUNCT_3:51;
then rng <:(diff (u,1,Z)),(diff (v,1,Z)):> c= [#] [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):] by A12, XBOOLE_1:1;
then reconsider w1 = <:(diff (u,1,Z)),(diff (v,1,Z)):> as PartFunc of S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):] by A11, RELSET_1:4;
A13: diff (u,1,Z) is_differentiable_on Z by A1, NDIFF_6:14;
A14: diff (v,1,Z) is_differentiable_on Z by A1, NDIFF_6:14;
A15: ( diff (w1,0,Z) is_differentiable_on Z & ex T1 being Lipschitzian LinearOperator of [:(diff_SP (1,S,(diff_SP (1,S,E)))),(diff_SP (1,S,(diff_SP (1,S,F)))):],(diff_SP (1,S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):])) st
( T1 = CTP (S,(diff_SP (0,S,(diff_SP (1,S,E)))),(diff_SP (0,S,(diff_SP (1,S,F))))) & diff (w1,1,Z) = T1 * <:(diff ((diff (u,1,Z)),1,Z)),(diff ((diff (v,1,Z)),1,Z)):> ) ) by A13, A14, Th58;
A16: diff_SP (0,S,(diff_SP (1,S,E))) = diff_SP (1,S,E) by NDIFF_6:7;
A17: diff_SP (0,S,(diff_SP (1,S,F))) = diff_SP (1,S,F) by NDIFF_6:7;
A18: diff ((diff (u,1,Z)),1,Z) = ((diff (u,1,Z)) | Z) `| Z by NDIFF_6:11
.= (diff (u,1,Z)) `| Z by A1, Th4, NDIFF_6:14
.= diff (u,(1 + 1),Z) by NDIFF_6:13 ;
A19: diff ((diff (v,1,Z)),1,Z) = ((diff (v,1,Z)) | Z) `| Z by NDIFF_6:11
.= (diff (v,1,Z)) `| Z by A1, Th4, NDIFF_6:14
.= diff (v,(1 + 1),Z) by NDIFF_6:13 ;
A20: diff_SP (0,S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):]) = [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):] by NDIFF_6:7;
A21: diff (w1,0,Z) = w1 | Z by NDIFF_6:11;
then A22: w1 | Z is_differentiable_on Z by A13, A14, A20, Th58;
w1 is_differentiable_on Z by Th3, A22;
then A23: w1 is_differentiable_on 1,Z by A13, A14, A20, A21, Th58, NDIFF_6:15;
set K = R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (0,S,E)),(diff_SP (0,S,F)):]);
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 reconsider L = 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)):],(R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (0,S,E)),(diff_SP (0,S,F)):])) ;
A24: diff_SP (0,S,E) = E by NDIFF_6:7;
A25: diff_SP (0,S,F) = F by NDIFF_6:7;
A26: R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (0,S,E)),(diff_SP (0,S,F)):]) = diff_SP (1,S,[:E,F:]) by A24, A25, NDIFF_6:7;
diff (w,1,Z) is_differentiable_on 1,Z by A4, A23, Th25;
then A27: ( Z c= dom (diff (w,1,Z)) & (diff (w,1,Z)) | Z is_differentiable_on Z ) by NDIFF_6:15;
then A28: diff (w,1,Z) is_differentiable_on Z ;
A29: R_NormSpace_of_BoundedLinearOperators (S,[:E,F:]) = diff_SP (1,S,[:E,F:]) by NDIFF_6:7;
diff (w,1,Z) = (w | Z) `| Z by NDIFF_6:11;
then (w | Z) `| Z is_differentiable_on Z by A27, A29;
hence w is_differentiable_on 2,Z by A7, A8, NDIFF_6:16; :: thesis:
reconsider L1 = L as Lipschitzian LinearOperator of [:(diff_SP (1,S,E)),(diff_SP (1,S,F)):],(diff_SP (1,S,[:E,F:])) by A26;
A30: CTP (S,(diff_SP (1,S,E)),(diff_SP (1,S,F))) is Lipschitzian LinearOperator of [:(diff_SP ((1 + 1),S,E)),(diff_SP ((1 + 1),S,F)):],(R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):])) by Th56;
R_NormSpace_of_BoundedLinearOperators (S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):]) = diff_SP (1,S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):]) by NDIFF_6:7;
then reconsider L2 = CTP (S,(diff_SP (1,S,E)),(diff_SP (1,S,F))) as Lipschitzian LinearOperator of [:(diff_SP (2,S,E)),(diff_SP (2,S,F)):],(diff_SP (1,S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):])) by A30;
diff_SP (1,S,(diff_SP (1,S,[:E,F:]))) = R_NormSpace_of_BoundedLinearOperators (S,(diff_SP (1,S,[:E,F:]))) by NDIFF_6:7
.= R_NormSpace_of_BoundedLinearOperators (S,(R_NormSpace_of_BoundedLinearOperators (S,[:E,F:]))) by NDIFF_6:7
.= diff_SP (2,S,[:E,F:]) by NDIFF_6:7 ;
then reconsider H = LTRN (1,L1,S) as Lipschitzian LinearOperator of (diff_SP (1,S,[:(diff_SP (1,S,E)),(diff_SP (1,S,F)):])),(diff_SP (2,S,[:E,F:])) ;
reconsider T = H * L2 as Lipschitzian LinearOperator of [:(diff_SP (2,S,E)),(diff_SP (2,S,F)):],(diff_SP (2,S,[:E,F:])) by LOPBAN_2:2;
take L1 ; :: thesis:
take L2 ; :: thesis:
take T ; :: thesis:
thus L1 = CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F))) ; :: thesis:
thus L2 = CTP (S,(diff_SP (1,S,E)),(diff_SP (1,S,F))) ; :: thesis:
thus T = (LTRN (1,L1,S)) * L2 ; :: thesis:
thus diff (w,2,Z) = diff (w,(1 + 1),Z)
.= (diff (w,1,Z)) `| Z by NDIFF_6:13
.= ((diff (w,1,Z)) | Z) `| Z by Th4, A28
.= diff ((L * w1),1,Z) by A4, A26, NDIFF_6:11
.= (LTRN (1,L1,S)) * (diff (w1,1,Z)) by A23, A26, Th25
.= T * <:(diff (u,2,Z)),(diff (v,2,Z)):> by A15, A16, A17, A18, A19, RELAT_1:36 ; :: thesis: