:: deftheorem Def35 defines categorical_exponent CAT_8:def 35 :
for C1, C2 being category
for b₃ being pair object holds
( b₃ is categorical_exponent of C1,C2 iff ex C being category ex E being Functor of (C [x] C1),C2 st
( b₃ = [C,E] & E is covariant & C,E is_exponent_of C1,C2 ) );