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:19;

now

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
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;

now

assume fs . k <> 0 ; :: thesis: contradiction
then A5: 0 < fs . k1 ;
for k being Nat st k in dom fs holds
0 <= fs . k ;
hence contradiction by A1, A2, A4, A5, RVSUM_1:115; :: thesis: verum

end;

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

end;

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

end;

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