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