scheme :: STIRL2_1:sch 2
Sch2{ F₁() -> set , F₂() -> set , F₃() -> set , F₄() -> set , F₅() -> Function of F₁(),F₂(), F₆( object ) -> object } :

ex h being Function of F₃(),F₄() st
( h | F₁() = F₅() & ( for x being set st x in F₃() \ F₁() holds
h . x = F₆(x) ) )

provided

A1: for x being set st x in F₃() \ F₁() holds
F₆(x) in F₄() and
A2: ( F₁() c= F₃() & F₂() c= F₄() ) and
A3: ( F₂() is empty implies F₁() is empty )