scheme :: PARTFUN1:sch 3
LambdaR{ F₁() -> set , F₂() -> set , F₃( object ) -> object , P₁[ object ] } :

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

provided

A1: for x being object st P₁[x] holds
F₃(x) in F₂()