:: deftheorem Def3 defines unital AOFA_000:def 3 :
for f being homogeneous Function holds
( f is unital iff ex x being set st x is_a_unity_wrt f );