let fs be FinSequence of NAT ; :: thesis: ( Sum fs = 0 iff fs = (len fs) |-> 0 )

hence Sum fs = 0 by RVSUM_1:81; :: thesis: verum

hereby :: thesis: ( fs = (len fs) |-> 0 implies Sum fs = 0 )

assume
fs = (len fs) |-> 0
; :: thesis: Sum fs = 0 assume A1:
Sum fs = 0
; :: thesis: fs = (len fs) |-> 0

A2: Seg (len fs) = dom fs by FINSEQ_1:def 3;

A3: Seg (len fs) = dom ((len fs) |-> 0) by FUNCOP_1:13;

end;A2: Seg (len fs) = dom fs by FINSEQ_1:def 3;

A3: Seg (len fs) = dom ((len fs) |-> 0) by FUNCOP_1:13;

now :: thesis: for k being Nat st k in Seg (len fs) holds

fs . k = ((len fs) |-> 0) . k

hence
fs = (len fs) |-> 0
by A2, A3, FINSEQ_1:13; :: thesis: verumfs . k = ((len fs) |-> 0) . k

let k be Nat; :: thesis: ( k in Seg (len fs) implies fs . k = ((len fs) |-> 0) . k )

assume A4: k in Seg (len fs) ; :: thesis: fs . k = ((len fs) |-> 0) . k

end;assume A4: k in Seg (len fs) ; :: thesis: fs . k = ((len fs) |-> 0) . k

now :: thesis: not fs . k <> 0

hence
fs . k = ((len fs) |-> 0) . k
by A4, FUNCOP_1:7; :: thesis: verumassume A5:
fs . k <> 0
; :: thesis: contradiction

for k being Nat st k in dom fs holds

0 <= fs . k ;

hence contradiction by A1, A2, A4, A5, RVSUM_1:85; :: thesis: verum

end;for k being Nat st k in dom fs holds

0 <= fs . k ;

hence contradiction by A1, A2, A4, A5, RVSUM_1:85; :: thesis: verum

hence Sum fs = 0 by RVSUM_1:81; :: thesis: verum