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