let RS be RealLinearSpace; :: thesis: for f being FinSequence of RS st f = (Seg (len f)) --> (0. RS) holds
Sum f = 0. RS
let f be FinSequence of RS; :: thesis: ( f = (Seg (len f)) --> (0. RS) implies Sum f = 0. RS )
assume AS: f = (Seg (len f)) --> (0. RS) ; :: thesis: Sum f = 0. RS

X1: now

let k be Element of NAT ; :: thesis: for v being Element of RS st k in dom f & v = f . k holds
f . k = - v
let v be Element of RS; :: thesis: ( k in dom f & v = f . k implies f . k = - v )
assume P214: ( k in dom f & v = f . k ) ; :: thesis: f . k = - v
then k in Seg (len f) by FINSEQ_1:def 3;
then f . k = 0. RS by AS, FUNCOP_1:13;
hence f . k = - v by P214, RLVECT_1:25; :: thesis: verum

end;

len f = len f ;
then Sum f = - (Sum f) by X1, RLVECT_1:57;
hence Sum f = 0. RS by RLVECT_1:33; :: thesis: verum