for f1, f2 being Ordinal-Sequence st f1 is increasing & f2 is increasing holds
ex phi being Ordinal-Sequence st
( phi = f1 * f2 & phi is increasing )