let X be set ; :: thesis: for G being non empty multMagma holds .: (G,X) is constituted-Functions

let G be non empty multMagma ; :: thesis: .: (G,X) is constituted-Functions

let a be Element of (.: (G,X)); :: according to MONOID_0:def 1 :: thesis: a is set

a is Element of Funcs (X,H_{3}(G))
by Th17;

hence a is set ; :: thesis: verum

let G be non empty multMagma ; :: thesis: .: (G,X) is constituted-Functions

let a be Element of (.: (G,X)); :: according to MONOID_0:def 1 :: thesis: a is set

a is Element of Funcs (X,H

hence a is set ; :: thesis: verum