:: deftheorem defines with_right_units ALTCAT_1:def 6 :
for I being non empty set
for G being ManySortedSet of [:I,I:]
for IT being BinComp of G holds
( IT is with_right_units iff for i being Element of I ex e being set st
( e in G . (i,i) & ( for j being Element of I
for f being set st f in G . (i,j) holds
(IT . (i,i,j)) . (f,e) = f ) ) );