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

provided

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