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