let F, G be FinSequence; :: thesis: ( len F = len G & ( for i being Nat st i in dom F holds
F . i = G . i ) implies F = G )
assume that
A1: len F = len G and
A2: for i being Nat st i in dom F holds
F . i = G . i ; :: thesis: F = G
A3: dom F = Seg (len F) by FINSEQ_1:def 3;
dom G = Seg (len F) by A1, FINSEQ_1:def 3;
hence F = G by A2, A3, FINSEQ_1:17; :: thesis: verum