let X be non empty set ; :: thesis: for s being FinSequence of (bspace X)

for x being Element of X holds (Sum s) @ x = Sum (s @ x)

let s be FinSequence of (bspace X); :: thesis: for x being Element of X holds (Sum s) @ x = Sum (s @ x)

let x be Element of X; :: thesis: (Sum s) @ x = Sum (s @ x)

set V = bspace X;

defpred S_{1}[ FinSequence of (bspace X)] means (Sum $1) @ x = Sum ($1 @ x);

A1: S_{1}[ <*> (bspace X)]

for f being Element of (bspace X) st S_{1}[p] holds

S_{1}[p ^ <*f*>]
_{1}[p]
from BSPACE:sch 1(A1, A3);

hence (Sum s) @ x = Sum (s @ x) ; :: thesis: verum

for x being Element of X holds (Sum s) @ x = Sum (s @ x)

let s be FinSequence of (bspace X); :: thesis: for x being Element of X holds (Sum s) @ x = Sum (s @ x)

let x be Element of X; :: thesis: (Sum s) @ x = Sum (s @ x)

set V = bspace X;

defpred S

A1: S

proof

A3:
for p being FinSequence of (bspace X)
reconsider z = 0. (bspace X) as Subset of X ;

set e = <*> (bspace X);

A2: z @ x = 0. Z_2 by Def3;

( Sum (<*> (bspace X)) = 0. (bspace X) & (<*> (bspace X)) @ x = <*> Z_2 ) by Th31, RLVECT_1:43;

hence S_{1}[ <*> (bspace X)]
by A2, RLVECT_1:43; :: thesis: verum

end;set e = <*> (bspace X);

A2: z @ x = 0. Z_2 by Def3;

( Sum (<*> (bspace X)) = 0. (bspace X) & (<*> (bspace X)) @ x = <*> Z_2 ) by Th31, RLVECT_1:43;

hence S

for f being Element of (bspace X) st S

S

proof

for p being FinSequence of (bspace X) holds S
let p be FinSequence of (bspace X); :: thesis: for f being Element of (bspace X) st S_{1}[p] holds

S_{1}[p ^ <*f*>]

let f be Element of (bspace X); :: thesis: ( S_{1}[p] implies S_{1}[p ^ <*f*>] )

assume A4: S_{1}[p]
; :: thesis: S_{1}[p ^ <*f*>]

(Sum (p ^ <*f*>)) @ x = ((Sum p) + (Sum <*f*>)) @ x by RLVECT_1:41

.= ((Sum p) + f) @ x by RLVECT_1:44

.= ((Sum p) @ x) + (f @ x) by Th32

.= (Sum (p @ x)) + (Sum <*(f @ x)*>) by A4, RLVECT_1:44

.= Sum ((p @ x) ^ <*(f @ x)*>) by RLVECT_1:41

.= Sum ((p ^ <*f*>) @ x) by Th33 ;

hence S_{1}[p ^ <*f*>]
; :: thesis: verum

end;S

let f be Element of (bspace X); :: thesis: ( S

assume A4: S

(Sum (p ^ <*f*>)) @ x = ((Sum p) + (Sum <*f*>)) @ x by RLVECT_1:41

.= ((Sum p) + f) @ x by RLVECT_1:44

.= ((Sum p) @ x) + (f @ x) by Th32

.= (Sum (p @ x)) + (Sum <*(f @ x)*>) by A4, RLVECT_1:44

.= Sum ((p @ x) ^ <*(f @ x)*>) by RLVECT_1:41

.= Sum ((p ^ <*f*>) @ x) by Th33 ;

hence S

hence (Sum s) @ x = Sum (s @ x) ; :: thesis: verum