scheme :: BINOP_1:sch 5
PartFuncEx2{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ object , object , object ] } :

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

provided

A1: for x, y, z being object st x in F₁() & y in F₂() & P₁[x,y,z] holds
z in F₃() and
A2: for x, y, z1, z2 being object st x in F₁() & y in F₂() & P₁[x,y,z1] & P₁[x,y,z2] holds
z1 = z2