theorem Th8: :: BINOM:8
for R being non empty unital multMagma
for a being Element of R holds
( a |^ 0 = 1_ R & a |^ 1 = a )