scheme :: RLVECT_4:sch 1
LambdaSep3{ 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₇() -> Element of F₂(), F₈() -> Element of F₂(), F₉( set ) -> Element of F₂() } :

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

provided

A1: F₃() <> F₄() and
A2: F₃() <> F₅() and
A3: F₄() <> F₅()