theorem Th19: :: MONOID_1:19

for X being set
for G being non empty multMagma
for f being Element of (.: (G,X)) holds
( dom f = X & rng f c= the carrier of G )