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