let p, q be FinSequence; :: thesis: ( ( p c= q or dom p c= dom q ) implies len p <= len q )
assume ( p c= q or dom p c= dom q ) ; :: thesis: len p <= len q
then dom p c= dom q by RELAT_1:11;
then A1: Segm (card (dom p)) c= Segm (card (dom q)) by CARD_1:11;
( card (dom p) = card p & card (dom q) = card q ) by CARD_1:62;
hence len p <= len q by A1, NAT_1:39; :: thesis: verum