for f1, f2 being Ordinal-Sequence st f1 is increasing holds
f2 * f1 is Ordinal-Sequence