theorem Th7: :: TOPREAL8:7

for f, g being FinSequence holds len f <= len (f ^' g)