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;

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

hence
F1 = F2
by A3, A5, FINSEQ_2:9; :: thesis: verumF1 . 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;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