let F1, F2 be FinSequence of V1; :: thesis: ( len F1 = len M & ( for k being Nat st k in dom F1 holds
F1 /. k = Sum (M /. k) ) & len F2 = len M & ( for k being Nat st k in dom F2 holds
F2 /. k = Sum (M /. k) ) implies F1 = F2 )
assume that
A3: len F1 = len M and
A4: for k being Nat st k in dom F1 holds
F1 /. k = Sum (M /. k) and
A5: len F2 = len M and
A6: for k being Nat st k in dom F2 holds
F2 /. k = Sum (M /. k) ; :: thesis: F1 = F2
A7: dom F1 = Seg (len F1) by FINSEQ_1:def 3;

now :: thesis: for k being Nat st k in dom F1 holds
F1 . k = F2 . k

let k be Nat; :: thesis: ( k in dom F1 implies F1 . k = F2 . k )
assume A8: k in dom F1 ; :: thesis: F1 . k = F2 . k
then A9: k in dom F2 by A3, A5, A7, FINSEQ_1:def 3;
thus F1 . k = F1 /. k by A8, PARTFUN1:def 6
.= Sum (M /. k) by A4, A8
.= F2 /. k by A6, A9
.= F2 . k by A9, PARTFUN1:def 6 ; :: thesis: verum

end;

hence F1 = F2 by A3, A5, FINSEQ_2:9; :: thesis: verum