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_{3}(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

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

f = f ;

hence ( dom f = X & rng f c= the carrier of G ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum