let G be RealNormSpace-Sequence; :: thesis:
let X be non empty open Subset of (product G); :: thesis:
let F be RealNormSpace; :: thesis:
let f be PartFunc of (product G),F; :: thesis:
defpred S₁[ Nat] means for F being RealNormSpace
for f being PartFunc of (product G),F st 1 <= $1 & ( for I being non empty FinSequence of dom G st len I <= $1 holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) ) holds
( f is_differentiable_on $1,X & diff (f,$1,X) is_continuous_on X );
A2: S₁[ 0 ] ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
let F be RealNormSpace; :: thesis:
let f be PartFunc of (product G),F; :: thesis:
assume A5: ( 1 <= n + 1 & ( for I being non empty FinSequence of dom G st len I <= n + 1 holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) ) ) ; :: thesis:
A6: for i being set st i in dom G holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X )

let i be set ; :: thesis:
assume i in dom G ; :: thesis:
then reconsider i0 = i as Element of dom G ;
set I = <*i0*>;
A7: ( len <*i0*> = 1 & <*i0*> . 1 = i0 ) by FINSEQ_1:40;
reconsider I = <*i0*> as non empty FinSequence of dom G ;
A8: ( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) by A5, A7;
hence f is_partial_differentiable_on X,i ; :: thesis:
Partdiff_SP (G,F,I,(len I)) = R_NormSpace_of_BoundedLinearOperators ((G . (In (i0,(dom G)))),F) by A7, Th12;
hence f `partial| (X,i) is_continuous_on X by A8, Th15; :: thesis:

end;

then A10: ( f is_differentiable_on X & f `| X is_continuous_on X ) by NDIFF_5:57;

per cases ;

suppose A11: n = 0 ; :: thesis:

hence f is_differentiable_on n + 1,X by A10, NDIFF_6:15, NDIFF13:2; :: thesis:
diff (f,(n + 1),X) = (f | X) `| X by A11, NDIFF_6:11
.= f `| X by A10, NDIFF13:3 ;
hence diff (f,(n + 1),X) is_continuous_on X by A10, A11, NDIFF_6:7; :: thesis:

end;

suppose A14: n <> 0 ; :: thesis:

then A15: 1 <= n by NAT_1:14;
A16: for i being set st i in dom G holds
( f `partial| (X,i) is_differentiable_on n,X & diff ((f `partial| (X,i)),n,X) is_continuous_on X )

proof

let i be set ; :: thesis:
assume i in dom G ; :: thesis:
then reconsider i0 = i as Element of dom G ;
set J1 = <*i0*>;
A17: ( <*i0*> . 1 = i0 & len <*i0*> = 1 ) by FINSEQ_1:40;
reconsider J1 = <*i0*> as non empty FinSequence of dom G ;
for J2 being non empty FinSequence of dom G st len J2 <= n holds
( f `partial| (X,i) is_partial_differentiable_on X,J2 & (f `partial| (X,i)) `partial| (X,J2) is_continuous_on X )

proof

let J2 be non empty FinSequence of dom G; :: thesis:
assume A18: len J2 <= n ; :: thesis:
set I = J1 ^ J2;
len (J1 ^ J2) = (len J1) + (len J2) by FINSEQ_1:22;
then len (J1 ^ J2) <= n + 1 by A17, A18, XREAL_1:7;
then A19: ( f is_partial_differentiable_on X,J1 ^ J2 & f `partial| (X,(J1 ^ J2)) is_continuous_on X ) by A5;
A20: ( f is_partial_differentiable_on X,J1 & f `partial| (X,J1) is_partial_differentiable_on X,J2 ) by A19, Th20;
A21: ( (f `partial| (X,J1)) `partial| (X,J2) = f `partial| (X,(J1 ^ J2)) & Partdiff_SP (G,(Partdiff_SP (G,F,J1,(len J1))),J2,(len J2)) = Partdiff_SP (G,F,(J1 ^ J2),(len (J1 ^ J2))) ) by Th18;
A22: Partdiff_SP (G,F,J1,(len J1)) = R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F) by A17, Th12;
hence f `partial| (X,i) is_partial_differentiable_on X,J2 by A20, Th15; :: thesis:
thus (f `partial| (X,i)) `partial| (X,J2) is_continuous_on X by A19, A21, A22, Th15; :: thesis:

end;

hence ( f `partial| (X,i) is_differentiable_on n,X & diff ((f `partial| (X,i)),n,X) is_continuous_on X ) by A4, A15; :: thesis:

end;

A25: for x being Point of (product G) st x in X holds
for dx being Point of (product G) ex w being FinSequence of F st
( dom w = dom G & ( for i being set st i in dom G holds
w . i = ((f `partial| (X,i)) /. x) . ((proj (In (i,(dom G)))) . dx) ) & ((f `| X) /. x) . dx = Sum w )

proof

let x be Point of (product G); :: thesis:
assume A26: x in X ; :: thesis:
let dx be Point of (product G); :: thesis:
consider w being FinSequence of F such that
A27: ( dom w = dom G & ( for i being set st i in dom G holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . dx) ) & (diff (f,x)) . dx = Sum w ) by A6, A26, NDIFF_5:56;
take w ; :: thesis:
thus dom w = dom G by A27; :: thesis:
thus for i being set st i in dom G holds
w . i = ((f `partial| (X,i)) /. x) . ((proj (In (i,(dom G)))) . dx) :: thesis:

proof

let i be set ; :: thesis:
assume A28: i in dom G ; :: thesis:
then A29: w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . dx) by A27;
f is_partial_differentiable_on X,i by A6, A28;
hence w . i = ((f `partial| (X,i)) /. x) . ((proj (In (i,(dom G)))) . dx) by A26, A29, NDIFF_5:def 9; :: thesis:

end;

thus ((f `| X) /. x) . dx = Sum w by A10, A26, A27, NDIFF_1:def 9; :: thesis:

end;

set GF = R_NormSpace_of_BoundedLinearOperators ((product G),F);
A30: for i being set st i in dom G holds
ex Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) st
( Wi is_differentiable_on n,X & diff (Wi,n,X) is_continuous_on X & dom Wi = X & ( for x being Point of (product G) st x in X holds
Wi . x = ((f `partial| (X,i)) /. x) * (proj (In (i,(dom G)))) ) )

proof

proof

let x be Point of (product G); :: thesis:
assume A44: x in X ; :: thesis:
reconsider fpi = (f `partial| (X,i)) /. x as Lipschitzian LinearOperator of (G . (In (i,(dom G)))),F by LOPBAN_1:def 9;
reconsider fLi = Li as Lipschitzian LinearOperator of (product G),(G . (In (i,(dom G)))) by LOPBAN_1:def 9;
A45: modetrans (fpi,(G . (In (i,(dom G)))),F) = (f `partial| (X,i)) /. x by LOPBAN_1:def 11;
thus W . x = B . (w . x) by A43, A44, FUNCT_1:12
.= B . [(L . x),((f `partial| (X,i)) . x)] by A32, A34, A44, FUNCT_3:49
.= B . [Li,((f `partial| (X,i)) . x)] by A44, FUNCOP_1:7
.= B . (Li,((f `partial| (X,i)) /. x)) by A34, A44, PARTFUN1:def 6
.= ((f `partial| (X,i)) /. x) * Li by A33
.= ((f `partial| (X,i)) /. x) * (proj (In (i,(dom G)))) by A45, LOPBAN_1:def 11 ; :: thesis:

end;

hence ( W is_differentiable_on n,X & diff (W,n,X) is_continuous_on X & dom W = X & ( for x being Point of (product G) st x in X holds
W . x = ((f `partial| (X,i)) /. x) * (proj (In (i,(dom G)))) ) ) by A35, A36, A37, A38, A39, A40, A41, A42, NDIFF13:41, RELAT_1:27, XBOOLE_1:1; :: thesis:

end;

set PGF = R_NormSpace_of_BoundedLinearOperators ((product G),F);
defpred S₂[ object , object ] means ex Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) st
( $2 = Wi & Wi is_differentiable_on n,X & diff (Wi,n,X) is_continuous_on X & dom Wi = X & ( for x being Point of (product G) st x in X holds
Wi . x = ((f `partial| (X,(In ($1,(dom G))))) /. x) * (proj (In ($1,(dom G)))) ) );
A47: for i being object st i in dom G holds
ex y being object st
( y in PFuncs ( the carrier of (product G), the carrier of (R_NormSpace_of_BoundedLinearOperators ((product G),F))) & S₂[i,y] )

proof

let i be object ; :: thesis:
assume A48: i in dom G ; :: thesis:
reconsider i0 = i as set by TARSKI:1;
consider Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) such that
A49: ( Wi is_differentiable_on n,X & diff (Wi,n,X) is_continuous_on X & dom Wi = X & ( for x being Point of (product G) st x in X holds
Wi . x = ((f `partial| (X,i0)) /. x) * (proj (In (i,(dom G)))) ) ) by A30, A48;
take y = Wi; :: thesis:
In (i,(dom G)) = i by A48, SUBSET_1:def 8;
hence ( y in PFuncs ( the carrier of (product G), the carrier of (R_NormSpace_of_BoundedLinearOperators ((product G),F))) & S₂[i,y] ) by A49, PARTFUN1:45; :: thesis:

end;

A51: the carrier of (product G) --> (0. (R_NormSpace_of_BoundedLinearOperators ((product G),F))) in PFuncs ( the carrier of (product G), the carrier of (R_NormSpace_of_BoundedLinearOperators ((product G),F))) by PARTFUN1:45;
consider W being Function of (dom G),(PFuncs ( the carrier of (product G), the carrier of (R_NormSpace_of_BoundedLinearOperators ((product G),F)))) such that
A52: for i being object st i in dom G holds
S₂[i,W . i] from FUNCT_2:sch 1(A47);
A53: for i being set st i in dom G holds
ex Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) st
( W . i = Wi & Wi is_differentiable_on n,X & diff (Wi,n,X) is_continuous_on X & dom Wi = X & ( for x being Point of (product G) st x in X holds
(W . i) . x = ((f `partial| (X,i)) /. x) * (proj (In (i,(dom G)))) ) )

proof

let i be set ; :: thesis:
assume A54: i in dom G ; :: thesis:
then consider Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) such that
A55: ( W . i = Wi & Wi is_differentiable_on n,X & diff (Wi,n,X) is_continuous_on X & dom Wi = X & ( for x being Point of (product G) st x in X holds
Wi . x = ((f `partial| (X,(In (i,(dom G))))) /. x) * (proj (In (i,(dom G)))) ) ) by A52;
take Wi ; :: thesis:
In (i,(dom G)) = i by A54, SUBSET_1:def 8;
hence ( W . i = Wi & Wi is_differentiable_on n,X & diff (Wi,n,X) is_continuous_on X & dom Wi = X & ( for x being Point of (product G) st x in X holds
(W . i) . x = ((f `partial| (X,i)) /. x) * (proj (In (i,(dom G)))) ) ) by A55; :: thesis:

end;

reconsider nn = n as non empty Nat by A14;
A56: dom W = dom G by A51, FUNCT_2:def 1
.= Seg (len G) by FINSEQ_1:def 3 ;
then reconsider W0 = W as FinSequence by FINSEQ_1:def 2;
for i being Nat st i in dom W0 holds
W0 . i in the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators ((product G),F)),nn))

proof

let i be Nat; :: thesis:
assume i in dom W0 ; :: thesis:
then consider Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) such that
A57: ( W . i = Wi & Wi is_differentiable_on n,X & diff (Wi,n,X) is_continuous_on X & dom Wi = X & ( for x being Point of (product G) st x in X holds
Wi . x = ((f `partial| (X,(In (i,(dom G))))) /. x) * (proj (In (i,(dom G)))) ) ) by A52, A56;
thus W0 . i in the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators ((product G),F)),nn)) by A57; :: thesis:

end;

then reconsider W0 = W0 as FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators ((product G),F)),nn)) by FINSEQ_2:12;
Sum W0 in the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators ((product G),F)),nn)) ;
then A58: ex f being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) st
( Sum W0 = f & dom f = X & f is_differentiable_on nn,X & diff (f,nn,X) is_continuous_on X ) ;
then reconsider Sw = Sum W0 as PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) ;
for x being Point of (product G) st x in dom (f `| X) holds
(f `| X) . x = Sw . x

proof

let x be Point of (product G); :: thesis:
assume A59: x in dom (f `| X) ; :: thesis:
then A60: x in X by A10, NDIFF_1:def 9;
then Sw . x = Sw /. x by A58, PARTFUN1:def 6;
then reconsider Swx = Sw . x as Lipschitzian LinearOperator of (product G),F by LOPBAN_1:def 9;
reconsider Fx = (f `| X) /. x as Lipschitzian LinearOperator of (product G),F by LOPBAN_1:def 9;
defpred S₃[ Nat, object ] means $2 = (W . $1) /. x;
A61: for k being Nat st k in Seg (len G) holds
ex x being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators ((product G),F)) st S₃[k,x] ;
consider Wx being FinSequence of the carrier of (R_NormSpace_of_BoundedLinearOperators ((product G),F)) such that
A62: ( dom Wx = Seg (len G) & ( for k being Nat st k in Seg (len G) holds
S₃[k,Wx . k] ) ) from FINSEQ_1:sch 5(A61);
A63: dom Wx = dom G by A62, FINSEQ_1:def 3;
A64: for i being Nat st i in dom Wx holds
Wx /. i = (W . i) /. x

proof

let i be Nat; :: thesis:
assume A65: i in dom Wx ; :: thesis:
then Wx . i = (W . i) /. x by A62;
hence Wx /. i = (W . i) /. x by A65, PARTFUN1:def 6; :: thesis:

end;

A66: dom Wx = dom W0 by A51, A63, FUNCT_2:def 1;
B66: for i being Nat st i in dom Wx holds
ex Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) st
( Wi = W0 . i & Wx /. i = Wi /. x )

proof

let i be Nat; :: thesis:
assume A67: i in dom Wx ; :: thesis:
consider Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) such that
A68: Wi = W . i ;
take Wi ; :: thesis:
thus ( Wi = W0 . i & Wx /. i = Wi /. x ) by A64, A67, A68; :: thesis:

end;

B69: for dx being Point of (product G) holds Fx . dx = Swx . dx

proof

let dx be Point of (product G); :: thesis:
consider w being FinSequence of F such that
A70: ( dom w = dom G & ( for i being set st i in dom G holds
w . i = ((f `partial| (X,i)) /. x) . ((proj (In (i,(dom G)))) . dx) ) & ((f `| X) /. x) . dx = Sum w ) by A25, A60;
for i being Nat st i in dom w holds
w . i = (Wx /. i) . dx

proof

let i be Nat; :: thesis:
assume A71: i in dom w ; :: thesis:
then A72: w . i = ((f `partial| (X,i)) /. x) . ((proj (In (i,(dom G)))) . dx) by A70;
consider Wi being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) such that
A73: ( W . i = Wi & Wi is_differentiable_on n,X & diff (Wi,n,X) is_continuous_on X & dom Wi = X & ( for x being Point of (product G) st x in X holds
(W . i) . x = ((f `partial| (X,i)) /. x) * (proj (In (i,(dom G)))) ) ) by A53, A70, A71;
A74: (W . i) . x = ((f `partial| (X,i)) /. x) * (proj (In (i,(dom G)))) by A60, A73;
A75: (W . i) . x = (W . i) /. x by A60, A73, PARTFUN1:def 6;
dom (proj (In (i,(dom G)))) = the carrier of (product G) by FUNCT_2:def 1;
hence w . i = ((W . i) /. x) . dx by A72, A74, A75, FUNCT_1:13
.= (Wx /. i) . dx by A63, A64, A70, A71 ;
:: thesis:

end;

then Sum w = (Sum Wx) . dx by A63, A70, Th2;
hence Fx . dx = Swx . dx by A60, A66, B66, A70, Th11; :: thesis:

end;

thus (f `| X) . x = (f `| X) /. x by A59, PARTFUN1:def 6
.= Sw . x by B69, FUNCT_2:63 ; :: thesis:

end;

then f `| X = Sum W0 by A10, A58, NDIFF_1:def 9;
then f `| X in the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators ((product G),F)),nn)) ;
then ex g being PartFunc of (product G),(R_NormSpace_of_BoundedLinearOperators ((product G),F)) st
( g = f `| X & dom g = X & g is_differentiable_on nn,X & diff (g,nn,X) is_continuous_on X ) ;
hence ( f is_differentiable_on n + 1,X & diff (f,(n + 1),X) is_continuous_on X ) by A10, NDIFF13:32; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence for n being Nat st 1 <= n holds
( ( f is_differentiable_on n,X & diff (f,n,X) is_continuous_on X ) iff for I being non empty FinSequence of dom G st len I <= n holds
( f is_partial_differentiable_on X,I & f `partial| (X,I) is_continuous_on X ) ) by Th35; :: thesis: