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 A1: f = (Seg (len f)) --> (0. RS) ; :: thesis: Sum f = 0. RS
A2: now :: thesis: for k being Nat
for v being Element of RS st k in dom f & v = f . k holds
f . k = - v
let k be 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 A3: ( 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 A1, FUNCOP_1:7;
hence f . k = - v by A3, RLVECT_1:12; :: thesis: verum
end;
len f = len f ;
then Sum f = - (Sum f) by A2, RLVECT_1:40;
hence Sum f = 0. RS by RLVECT_1:19; :: thesis: verum