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₁[ FinSequence of (bspace X)] means (Sum $1) @ x = Sum ($1 @ x);
A1: S₁[ <*> (bspace X)]

proof

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₁[ <*> (bspace X)] by A2, RLVECT_1:43; :: thesis: verum

end;

A3: for p being FinSequence of (bspace X)
for f being Element of (bspace X) st S₁[p] holds
S₁[p ^ <*f*>]

proof

let p be FinSequence of (bspace X); :: thesis: for f being Element of (bspace X) st S₁[p] holds
S₁[p ^ <*f*>]
let f be Element of (bspace X); :: thesis: ( S₁[p] implies S₁[p ^ <*f*>] )
assume A4: S₁[p] ; :: thesis: S₁[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₁[p ^ <*f*>] ; :: thesis: verum

end;

for p being FinSequence of (bspace X) holds S₁[p] from BSPACE:sch 1(A1, A3);
hence (Sum s) @ x = Sum (s @ x) ; :: thesis: verum