scheme :: FUNCT_2:sch 7
LambdaSep2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Element of F₂(), F₆() -> Element of F₂(), F₇( object ) -> Element of F₂() } :

ex f being Function of F₁(),F₂() st
( f . F₃() = F₅() & f . F₄() = F₆() & ( for x being Element of F₁() st x <> F₃() & x <> F₄() holds
f . x = F₇(x) ) )

provided

A1: F₃() <> F₄()