let p, q be FinSequence; :: thesis: ( len p <= len q iff dom p c= 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 c= dom q ) by FINSEQ_1:7; :: thesis: verum