:: deftheorem Def15 defines unital AOFA_000:def 15 :
for S being non-empty UAStr holds
( S is unital iff ex f being non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S st
( f = the charact of S . 2 & (Den ((In (1,(dom the charact of S))),S)) . {} is_a_unity_wrt f ) );