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 Th18;
hence a is set ; :: thesis: verum