let G0, F be RealNormSpace; :: thesis: for X being non empty open Subset of G0
for n being non empty Nat
for x being Point of G0 st x in X holds
for W0 being FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n))
for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x
let X be non empty open Subset of G0; :: thesis: for n being non empty Nat
for x being Point of G0 st x in X holds
for W0 being FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n))
for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x
let n be non empty Nat; :: thesis: for x being Point of G0 st x in X holds
for W0 being FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n))
for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x
let x be Point of G0; :: thesis: ( x in X implies for W0 being FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n))
for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x )
assume A1: x in X ; :: thesis: for W0 being FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n))
for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x
set G0F = R_NormSpace_of_BoundedLinearOperators (G0,F);
set XG0Fn = RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n);
defpred S1[ Nat] means for W0 being FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n))
for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st len Wx = $1 & dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x;
A2: S1[ 0 ]
proof
let W0 be FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n)); :: thesis: for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st len Wx = 0 & dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x
let Wx be FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)); :: thesis: ( len Wx = 0 & dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) implies Sum Wx = (Sum W0) . x )
assume A3: ( len Wx = 0 & dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) ) ; :: thesis: Sum Wx = (Sum W0) . x
A4: Wx = <*> the carrier of (R_NormSpace_of_BoundedLinearOperators (G0,F)) by A3;
then A5: Sum Wx = 0. (R_NormSpace_of_BoundedLinearOperators (G0,F)) by RLVECT_1:43;
W0 = <*> the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n)) by A3, A4;
then Sum W0 = 0. (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n)) by RLVECT_1:43
.= X --> (0. (R_NormSpace_of_BoundedLinearOperators (G0,F))) by Th10 ;
hence Sum Wx = (Sum W0) . x by A1, A5, FUNCOP_1:7; :: thesis: verum
end;
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
let W0 be FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n)); :: thesis: for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st len Wx = k + 1 & dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x
let Wx be FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)); :: thesis: ( len Wx = k + 1 & dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) implies Sum Wx = (Sum W0) . x )
assume A8: ( len Wx = k + 1 & dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) ) ; :: thesis: Sum Wx = (Sum W0) . x
set Wx1 = Wx | k;
set W01 = W0 | k;
A10: dom W0 = Seg (k + 1) by A8, FINSEQ_1:def 3;
then A11: len W0 = k + 1 by FINSEQ_1:def 3;
then A12: len (W0 | k) = k by FINSEQ_1:59, NAT_1:11;
A13: W0 | k = W0 | (Seg k) by FINSEQ_1:def 16;
then A14: W0 | k = W0 | (dom (W0 | k)) by A12, FINSEQ_1:def 3;
W0 /. (len W0) = W0 . (len W0) by A10, A11, FINSEQ_1:4, PARTFUN1:def 6;
then A15: Sum W0 = (Sum (W0 | k)) + (W0 /. (len W0)) by A11, A12, A14, RLVECT_1:38;
A16: dom Wx = Seg (k + 1) by A8, FINSEQ_1:def 3;
A18: len (Wx | k) = k by A8, FINSEQ_1:59, NAT_1:11;
A19: Wx | k = Wx | (Seg k) by FINSEQ_1:def 16;
then A20: Wx | k = Wx | (dom (Wx | k)) by A18, FINSEQ_1:def 3;
Wx /. (len Wx) = Wx . (len Wx) by A8, A16, FINSEQ_1:4, PARTFUN1:def 6;
then A22: Sum Wx = (Sum (Wx | k)) + (Wx /. (len Wx)) by A8, A18, A20, RLVECT_1:38;
A23: dom (Wx | k) = Seg k by A18, FINSEQ_1:def 3
.= dom (W0 | k) by A12, FINSEQ_1:def 3 ;
for i being Nat st i in dom (Wx | k) holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = (W0 | k) . i & (Wx | k) /. i = Wi /. x )
proof
let i be Nat; :: thesis: ( i in dom (Wx | k) implies ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = (W0 | k) . i & (Wx | k) /. i = Wi /. x ) )
assume A24: i in dom (Wx | k) ; :: thesis: ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = (W0 | k) . i & (Wx | k) /. i = Wi /. x )
then A25: i in Seg (len (Wx | k)) by FINSEQ_1:def 3;
Seg (len (Wx | k)) c= Seg (len Wx) by A8, A18, FINSEQ_1:5, NAT_1:11;
then A26: Seg (len (Wx | k)) c= dom Wx by FINSEQ_1:def 3;
A27: (Wx | k) /. i = (Wx | k) . i by A24, PARTFUN1:def 6
.= Wx . i by FUNCT_1:49, A25, A18, A19
.= Wx /. i by A25, A26, PARTFUN1:def 6 ;
consider Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) such that
A28: ( Wi = W0 . i & Wx /. i = Wi /. x ) by A8, A25, A26;
take Wi ; :: thesis: ( Wi = (W0 | k) . i & (Wx | k) /. i = Wi /. x )
thus ( Wi = (W0 | k) . i & (Wx | k) /. i = Wi /. x ) by A13, A18, A25, A27, A28, FUNCT_1:49; :: thesis: verum
end;
then A29: Sum (Wx | k) = (Sum (W0 | k)) . x by A7, A23, A18;
1 <= len Wx by A8, NAT_1:11;
then consider Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) such that
A30: ( Wi = W0 . (len Wx) & Wx /. (len Wx) = Wi /. x ) by A8, FINSEQ_3:25;
Sum (W0 | k) in Continuously_differentiable_Functions (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n) ;
then consider SS being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) such that
A31: ( SS = Sum (W0 | k) & dom SS = X & SS is_differentiable_on n,X & diff (SS,n,X) is_continuous_on X ) ;
W0 . (len Wx) = W0 /. (len Wx) by A8, A16, FINSEQ_1:4, PARTFUN1:def 6;
then W0 . (len Wx) in Continuously_differentiable_Functions (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n) ;
then A32: ex f being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( f = W0 . (len Wx) & dom f = X & f is_differentiable_on n,X & diff (f,n,X) is_continuous_on X ) ;
A33: dom (SS + Wi) = (dom SS) /\ (dom Wi) by VFUNCT_1:def 1
.= X by A30, A31, A32 ;
A34: Wi = W0 /. (len Wx) by A8, A16, A30, FINSEQ_1:4, PARTFUN1:def 6;
(Sum (W0 | k)) . x = SS /. x by A1, A31, PARTFUN1:def 6;
hence Sum Wx = (SS + Wi) /. x by A1, A22, A29, A30, A33, VFUNCT_1:def 1
.= (SS + Wi) . x by A1, A33, PARTFUN1:def 6
.= (Sum W0) . x by A8, A11, A15, A30, A31, A32, A34, Th7 ;
:: thesis: verum
end;
A36: for k being Nat holds S1[k] from NAT_1:sch 2(A2, A6);
 let W0 be FinSequence of the carrier of (RVectSp_Continuously_differentiable_Funcs (X,(R_NormSpace_of_BoundedLinearOperators (G0,F)),n)); :: thesis: for Wx being FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)) st dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) holds
Sum Wx = (Sum W0) . x
let Wx be FinSequence of (R_NormSpace_of_BoundedLinearOperators (G0,F)); :: thesis: ( dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) implies Sum Wx = (Sum W0) . x )
assume A37: ( dom Wx = dom W0 & ( for i being Nat st i in dom Wx holds
ex Wi being PartFunc of G0,(R_NormSpace_of_BoundedLinearOperators (G0,F)) st
( Wi = W0 . i & Wx /. i = Wi /. x ) ) ) ; :: thesis: Sum Wx = (Sum W0) . x
len Wx = len Wx ;
hence Sum Wx = (Sum W0) . x by A36, A37; :: thesis: verum