let p, q be FinSequence; :: thesis: ( len p = len q iff dom p = dom q )
( dom p = Seg (len p) & dom q = Seg (len q) ) by FINSEQ_1:def 3;
hence ( len p = len q iff dom p = dom q ) by FINSEQ_1:8; :: thesis: verum