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_{3}(G))),((H_{1}(G),H_{3}(G)) .: X) #) )
by Def3;

( G is unital implies .: (G,X) = multLoopStr(# (Funcs (X,H_{3}(G))),((H_{1}(G),H_{3}(G)) .: X),(X --> (the_unity_wrt H_{1}(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

( 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 is unital implies .: (G,X) = multLoopStr(# (Funcs (X,H

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