theorem :: FINSEQ_1:63

for p, q being FinSequence st p c= q holds
len p <= len q