scheme :: PARTFUN1:sch 2
PartFuncEx{ F₁() -> set , F₂() -> set , P₁[ object , object ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for x being object holds
( x in dom f iff ( x in F₁() & ex y being object st P₁[x,y] ) ) ) & ( for x being object st x in dom f holds
P₁[x,f . x] ) )

provided

A1: for x, y being object st x in F₁() & P₁[x,y] holds
y in F₂() and
A2: for x, y1, y2 being object st x in F₁() & P₁[x,y1] & P₁[x,y2] holds
y1 = y2