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

let s be FinSequence of (); :: 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 S1[ FinSequence of ()] means (Sum \$1) @ x = Sum (\$1 @ x);
A1: S1[ <*> ()]
proof
reconsider z = 0. () as Subset of X ;
set e = <*> ();
A2: z @ x = 0. Z_2 by Def3;
( Sum (<*> ()) = 0. () & (<*> ()) @ x = <*> Z_2 ) by ;
hence S1[ <*> ()] by ; :: thesis: verum
end;
A3: for p being FinSequence of ()
for f being Element of () st S1[p] holds
S1[p ^ <*f*>]
proof
let p be FinSequence of (); :: thesis: for f being Element of () st S1[p] holds
S1[p ^ <*f*>]

let f be Element of (); :: thesis: ( S1[p] implies S1[p ^ <*f*>] )
assume A4: S1[p] ; :: thesis: S1[p ^ <*f*>]
(Sum (p ^ <*f*>)) @ x = ((Sum p) + ()) @ 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
.= Sum ((p @ x) ^ <*(f @ x)*>) by RLVECT_1:41
.= Sum ((p ^ <*f*>) @ x) by Th33 ;
hence S1[p ^ <*f*>] ; :: thesis: verum
end;
for p being FinSequence of () holds S1[p] from BSPACE:sch 1(A1, A3);
hence (Sum s) @ x = Sum (s @ x) ; :: thesis: verum