scheme :: SEQ_1:sch 3
LambdaPFD9{ F₁() -> non empty set , F₂() -> non empty set , F₃( object ) -> Element of F₂(), P₁[ object ] } :

ex f being PartFunc of F₁(),F₂() st
( ( for d being Element of F₁() holds
( d in dom f iff P₁[d] ) ) & ( for d being Element of F₁() st d in dom f holds
f . d = F₃(d) ) )