scheme :: ZF_REFLE:sch 1
ALFA9Universe{ F1() -> Universe, F2() -> non empty set , P1[ set , set ] } :
ex F being Function st
( dom F = F2() & ( for d being Element of F2() ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) ) ) )
provided
A1: for d being Element of F2() ex a being Ordinal of F1() st P1[d,a]