let X be set ; :: thesis: 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 ; :: thesis: ( 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,H₃(G))),((H₁(G),H₃(G)) .: X) #) ) by Def3;
( G is unital implies .: (G,X) = multLoopStr(# (Funcs (X,H₃(G))),((H₁(G),H₃(G)) .: X),(X --> (the_unity_wrt H₁(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; :: thesis: verum