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

hereby :: thesis: ( fs = (len fs) |-> 0 implies 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;

now :: thesis: for k being Nat st k in Seg (len fs) holds
fs . 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

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

assume 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;

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

end;

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

end;

assume fs = (len fs) |-> 0 ; :: thesis: Sum fs = 0
hence Sum fs = 0 by RVSUM_1:81; :: thesis: verum