scheme :: ZF_REFLE:sch 2
OrdSeqOfUnivEx{ F₁() -> Universe, P₁[ object , object ] } :

ex phi being Ordinal-Sequence of F₁() st
for a being Ordinal of F₁() holds P₁[a,phi . a]

provided

A1: for a being Ordinal of F₁() ex b being Ordinal of F₁() st P₁[a,b]