scheme :: YELLOW18:sch 14
NatTransLambda{ F₁() -> category, F₂() -> category, F₃() -> covariant Functor of F₁(),F₂(), F₄() -> covariant Functor of F₁(),F₂(), F₅( object ) -> object } :

ex t being natural_transformation of F₃(),F₄() st
( F₃() is_naturally_transformable_to F₄() & ( for a being Object of F₁() holds t ! a = F₅(a) ) )

provided

A1: for a being Object of F₁() holds F₅(a) in <^(F₃() . a),(F₄() . a)^> and
A2: for a, b being Object of F₁() st <^a,b^> <> {} holds
for f being Morphism of a,b
for g1 being Morphism of (F₃() . a),(F₄() . a) st g1 = F₅(a) holds
for g2 being Morphism of (F₃() . b),(F₄() . b) st g2 = F₅(b) holds
g2 * (F₃() . f) = (F₄() . f) * g1