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

ex f being PartFunc of F₁(),F₂() st
( ( for c being Element of F₁() holds
( c in dom f iff ( P₁[c] or P₂[c] ) ) ) & ( 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) ) ) ) )

provided

A1: for c being Element of F₁() st P₁[c] & P₂[c] holds
F₃(c) = F₄(c)