theorem :: TOPREAL8:9

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