:: deftheorem defines with_right-zero QUANTAL1:def 3 :
for IT being non empty multMagma holds
( IT is with_right-zero iff ex b being Element of IT st
for a being Element of IT holds a * b = b );