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