scheme :: FINSET_1:sch 1
OLambdaC{ F₁() -> set , P₁[ object ], F₂( object ) -> object , F₃( object ) -> object } :

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