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 Th17;
f = f ;
hence ( dom f = X & rng f c= the carrier of G ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum