scheme :: FUNCT_2:sch 2
Lambda1{ F₁() -> set , F₂() -> set , F₃( object ) -> object } :

ex f being Function of F₁(),F₂() st
for x being object st x in F₁() holds
f . x = F₃(x)

provided

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