let X be set ; :: thesis: for G being non empty multMagma
for f being Element of (.: G,X) holds
( dom f = X & rng f c= the carrier of G )
let G be non empty multMagma ; :: thesis: for f being Element of (.: G,X) holds
( dom f = X & rng f c= the carrier of G )
let f be Element of (.: G,X); :: thesis: ( dom f = X & rng f c= the carrier of G )
reconsider f = f as Element of Funcs X,H₃(G) by Th18;
f = f ;
hence ( dom f = X & rng f c= the carrier of G ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum