let L, M be RealNormSpace; :: thesis: for s being Point of L
for w being FinSequence of M
for X being FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)) st dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) holds
Sum w = (Sum X) . s
let s be Point of L; :: thesis: for w being FinSequence of M
for X being FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)) st dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) holds
Sum w = (Sum X) . s
set LM = R_NormSpace_of_BoundedLinearOperators (L,M);
defpred S₁[ Nat] means for w being FinSequence of M
for X being FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)) st len w = $1 & dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) holds
Sum w = (Sum X) . s;
A1: S₁[ 0 ]

proof

let w be FinSequence of M; :: thesis: for X being FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)) st len w = 0 & dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) holds
Sum w = (Sum X) . s
let X be FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)); :: thesis: ( len w = 0 & dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) implies Sum w = (Sum X) . s )
assume A2: ( len w = 0 & dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) ) ; :: thesis: Sum w = (Sum X) . s
A3: w = <*> the carrier of M by A2;
then A4: Sum w = 0. M by RLVECT_1:43;
X = <*> the carrier of (R_NormSpace_of_BoundedLinearOperators (L,M)) by A2, A3;
then Sum X = 0. (R_NormSpace_of_BoundedLinearOperators (L,M)) by RLVECT_1:43
.= the carrier of L --> (0. M) by LOPBAN_1:31 ;
hence Sum w = (Sum X) . s by A4, FUNCOP_1:7; :: thesis: verum

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let w be FinSequence of M; :: thesis: for X being FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)) st len w = k + 1 & dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) holds
Sum w = (Sum X) . s
let X be FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)); :: thesis: ( len w = k + 1 & dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) implies Sum w = (Sum X) . s )
assume A7: ( len w = k + 1 & dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) ) ; :: thesis: Sum w = (Sum X) . s
set w1 = w | k;
set X1 = X | k;
A9: dom X = Seg (k + 1) by A7, FINSEQ_1:def 3;
then A10: len X = k + 1 by FINSEQ_1:def 3;
then A11: len (X | k) = k by FINSEQ_1:59, NAT_1:11;
A12: X | k = X | (Seg k) by FINSEQ_1:def 16;
then A13: X | k = X | (dom (X | k)) by A11, FINSEQ_1:def 3;
X /. (len X) = X . (len X) by A9, A10, FINSEQ_1:4, PARTFUN1:def 6;
then A14: Sum X = (Sum (X | k)) + (X /. (len X)) by A10, A11, A13, RLVECT_1:38;
A15: dom w = Seg (k + 1) by A7, FINSEQ_1:def 3;
A17: len (w | k) = k by A7, FINSEQ_1:59, NAT_1:11;
A18: w | k = w | (Seg k) by FINSEQ_1:def 16;
then A19: w | k = w | (dom (w | k)) by A17, FINSEQ_1:def 3;
w /. (len w) = w . (len w) by A15, A7, FINSEQ_1:4, PARTFUN1:def 6;
then A20: Sum w = (Sum (w | k)) + (w /. (len w)) by A7, A17, A19, RLVECT_1:38;
A21: dom (w | k) = Seg k by A17, FINSEQ_1:def 3
.= dom (X | k) by A11, FINSEQ_1:def 3 ;
for i being Nat st i in dom (w | k) holds
(w | k) . i = ((X | k) /. i) . s

proof

let i be Nat; :: thesis: ( i in dom (w | k) implies (w | k) . i = ((X | k) /. i) . s )
assume A22: i in dom (w | k) ; :: thesis: (w | k) . i = ((X | k) /. i) . s
then A23: i in Seg (len (w | k)) by FINSEQ_1:def 3;
Seg (len (w | k)) c= Seg (len w) by A7, A17, FINSEQ_1:5, NAT_1:11;
then A24: Seg (len (w | k)) c= dom w by FINSEQ_1:def 3;
A25: (w | k) . i = w . i by FUNCT_1:49, A23, A17, A18
.= (X /. i) . s by A7, A23, A24 ;
(X | k) /. i = (X | k) . i by A21, A22, PARTFUN1:def 6
.= X . i by A12, A17, A23, FUNCT_1:49
.= X /. i by A7, A23, A24, PARTFUN1:def 6 ;
hence (w | k) . i = ((X | k) /. i) . s by A25; :: thesis: verum

end;

then A26: Sum (w | k) = (Sum (X | k)) . s by A6, A21, A17;
1 <= len w by A7, NAT_1:11;
then A27: len w in dom w by FINSEQ_3:25;
then w . (len w) = (X /. (len w)) . s by A7;
then w /. (len w) = (X /. (len w)) . s by A27, PARTFUN1:def 6;
hence Sum w = (Sum X) . s by A7, A10, A14, A20, A26, LOPBAN_1:35; :: thesis: verum

end;

A29: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
let w be FinSequence of M; :: thesis: for X being FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)) st dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) holds
Sum w = (Sum X) . s
let X be FinSequence of (R_NormSpace_of_BoundedLinearOperators (L,M)); :: thesis: ( dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) implies Sum w = (Sum X) . s )
assume A30: ( dom w = dom X & ( for i being Nat st i in dom w holds
w . i = (X /. i) . s ) ) ; :: thesis: Sum w = (Sum X) . s
len w = len w ;
hence Sum w = (Sum X) . s by A29, A30; :: thesis: verum