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
A5: len F1 = len M and
A6: for k being Nat st k in dom F1 holds
F1 /. k = Sum (M /. k) and
A7: len F2 = len M and
A8: for k being Nat st k in dom F2 holds
F2 /. k = Sum (M /. k) ; :: thesis: F1 = F2
X: dom F1 = Seg (len F1) by FINSEQ_1:def 3;

now

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

end;

hence F1 = F2 by A5, A7, FINSEQ_2:10; :: thesis: verum