theorem Th28: :: FINSEQ_3:30

for p, q being FinSequence holds
( len p <= len q iff dom p c= dom q )