let n be Nat; :: thesis: for F being FinSequence of F_Real st F = (Seg n) --> (0. F_Real) holds

Sum F = 0. F_Real

let F be FinSequence of F_Real; :: thesis: ( F = (Seg n) --> (0. F_Real) implies Sum F = 0. F_Real )

assume AS: F = (Seg n) --> (0. F_Real) ; :: thesis: Sum F = 0. F_Real

X2: len F = len F ;

for k being Nat

for v being Element of F_Real st k in dom F & v = F . k holds

F . k = - v

hence Sum F = 0. F_Real ; :: thesis: verum

Sum F = 0. F_Real

let F be FinSequence of F_Real; :: thesis: ( F = (Seg n) --> (0. F_Real) implies Sum F = 0. F_Real )

assume AS: F = (Seg n) --> (0. F_Real) ; :: thesis: Sum F = 0. F_Real

X2: len F = len F ;

for k being Nat

for v being Element of F_Real st k in dom F & v = F . k holds

F . k = - v

proof

then
Sum F = - (Sum F)
by X2, RLVECT_1:40;
let k be Nat; :: thesis: for v being Element of F_Real st k in dom F & v = F . k holds

F . k = - v

let v be Element of F_Real; :: thesis: ( k in dom F & v = F . k implies F . k = - v )

assume that

X3: k in dom F and

X30: v = F . k ; :: thesis: F . k = - v

X2: k in Seg n by AS, X3, FUNCT_2:def 1;

then v = 0. F_Real by AS, X30, FUNCOP_1:7;

hence F . k = - v by AS, X2, FUNCOP_1:7; :: thesis: verum

end;F . k = - v

let v be Element of F_Real; :: thesis: ( k in dom F & v = F . k implies F . k = - v )

assume that

X3: k in dom F and

X30: v = F . k ; :: thesis: F . k = - v

X2: k in Seg n by AS, X3, FUNCT_2:def 1;

then v = 0. F_Real by AS, X30, FUNCOP_1:7;

hence F . k = - v by AS, X2, FUNCOP_1:7; :: thesis: verum

hence Sum F = 0. F_Real ; :: thesis: verum