scheme :: TARSKI:sch 1
Replacement{ F1() -> set , P1[ object , object ] } :
ex X being set st
for x being object holds
( x in X iff ex y being object st
( y in F1() & P1[y,x] ) )
provided
A1: for x, y, z being object st P1[x,y] & P1[x,z] holds
y = z