theorem Th20: :: MONOID_1:20
for X being set
for G being non empty multMagma
for f, g being Element of (.: (G,X)) st ( for x being object st x in X holds
f . x = g . x ) holds
f = g