let p, q be FinSequence; :: thesis: ( p c= q implies len p <= len q )
assume p c= q ; :: thesis: len p <= len q
then card p c= card q by CARD_1:27;
hence len p <= len q by NAT_1:40; :: thesis: verum