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
proof
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;
then Sum F = - (Sum F) by X2, RLVECT_1:40;
hence Sum F = 0. F_Real ; :: thesis: verum