scheme :: BINOP_1:sch 7
PartLambda2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( object , object ) -> object , P₁[ 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₂() & P₁[x,y] ) ) ) & ( for x, y being object st [x,y] in dom f holds
f . (x,y) = F₄(x,y) ) )

provided

A1: for x, y being object st x in F₁() & y in F₂() & P₁[x,y] holds
F₄(x,y) in F₃()