scheme :: ZF_REFLE:sch 2
OrdSeqOfUnivEx{ F1() -> Universe, P1[ object , object ] } :
ex phi being Ordinal-Sequence of F1() st
for a being Ordinal of F1() holds P1[a,phi . a]
provided
A1: for a being Ordinal of F1() ex b being Ordinal of F1() st P1[a,b]