scheme :: ORDINAL1:sch 6
ALFA{ F₁() -> non empty set , P₁[ object , object ] } :

ex F being Function st
( dom F = F₁() & ( for d being Element of F₁() ex A being Ordinal st
( A = F . d & P₁[d,A] & ( for B being Ordinal st P₁[d,B] holds
A c= B ) ) ) )

provided

A1: for d being Element of F₁() ex A being Ordinal st P₁[d,A]