theorem Th22: :: MONOID_1:22

for X being set
for G being non empty unital multMagma holds 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G)