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 A1: ( len F = len G & ( for i being Nat st i in dom F holds
F . i = G . i ) ) ; :: thesis: F = G
A2: 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 A1, A2, FINSEQ_1:17; :: thesis: verum