:: deftheorem Def3 defines <| YONEDA_1:def 3 :
for A being Category
for f being Morphism of A
for b₃ being natural_transformation of <|(cod f),?>,<|(dom f),?> holds
( b₃ = <|f,?> iff for o being Object of A holds b₃ . o = [[(Hom ((cod f),o)),(Hom ((dom f),o))],(hom (f,(id o)))] );