for phi being Ordinal-Sequence st ( for c being Ordinal st c in dom phi holds
phi . c = epsilon_ c ) holds
phi is increasing