scheme :: ORDINAL4:sch 2
UOSLambda{ F1() -> Universe, F2( set ) -> Ordinal of F1() } :
ex phi being Ordinal-Sequence of F1() st
for a being Ordinal of F1() holds phi . a = F2(a)