:: deftheorem Def12 defines Psi CATALG_1:def 12 :
for C1, C2 being Category
for F being Functor of C1,C2
for b₄ being Function of the carrier' of (CatSign the carrier of C1), the carrier' of (CatSign the carrier of C2) holds
( b₄ = Psi F iff for o being OperSymbol of (CatSign the carrier of C1) holds b₄ . o = [(o `1),((Obj F) * (o `2))] );