scheme :: PARTFUN1:sch 4
LambdaC9{ F₁() -> non empty set , P₁[ object ], F₂( object ) -> object , F₃( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for x being Element of F₁() holds
( ( P₁[x] implies f . x = F₂(x) ) & ( P₁[x] implies f . x = F₃(x) ) ) ) )