scheme :: ZF_REFLE:sch 1
ALFA9Universe{ F₁() -> Universe, F₂() -> non empty set , P₁[ set , set ] } :

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

provided

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