scheme :: FUNCTOR0:sch 1
ValOnPair{ F₁() -> non empty set , F₂() -> Function, F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅( object , object ) -> set , P₁[ object , object ] } :

F₂() . (F₃(),F₄()) = F₅(F₃(),F₄())

provided

A1: F₂() = { [[o,o9],F₅(o,o9)] where o, o9 is Element of F₁() : P₁[o,o9] } and
A2: P₁[F₃(),F₄()]