let X be set ; for G being non empty multMagma holds
( the carrier of (.: (G,X)) = Funcs (X, the carrier of G) & the multF of (.: (G,X)) = ( the multF of G, the carrier of G) .: X )
let G be non empty multMagma ; ( the carrier of (.: (G,X)) = Funcs (X, the carrier of G) & the multF of (.: (G,X)) = ( the multF of G, the carrier of G) .: X )
A1:
( not G is unital implies .: (G,X) = multMagma(# (Funcs (X,H3(G))),((H1(G),H3(G)) .: X) #) )
by Def3;
( G is unital implies .: (G,X) = multLoopStr(# (Funcs (X,H3(G))),((H1(G),H3(G)) .: X),(X --> (the_unity_wrt H1(G))) #) )
by Def3;
hence
( the carrier of (.: (G,X)) = Funcs (X, the carrier of G) & the multF of (.: (G,X)) = ( the multF of G, the carrier of G) .: X )
by A1; verum