scheme :: SCHEME1:sch 8
PartFuncExD299{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set ], F₃( set ) -> Element of F₂(), F₄( set ) -> Element of F₂() } :

ex f being PartFunc of F₁(),F₂() st
( f is total & ( for c being Element of F₁() st c in dom f holds
( ( P₁[c] implies f . c = F₃(c) ) & ( P₁[c] implies f . c = F₄(c) ) ) ) )