theorem Th9: :: ORDINAL6:9

for f1, f2 being Sequence holds f1 c= f1 ^ f2