theorem :: GROUP_2:35

for G being non empty multMagma
for a being Element of G holds
( ({} the carrier of G) * a = {} & a * ({} the carrier of G) = {} ) by Th16;