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₃(G)) by Th17;
hence a is set ; :: thesis: verum