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