let X be set ; :: thesis: for G being non empty unital multMagma holds 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G)
let G be non empty unital multMagma ; :: thesis: 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G)
.: (G,X) = multLoopStr(# (Funcs (X,H₃(G))),((H₁(G),H₃(G)) .: X),(X --> (the_unity_wrt H₁(G))) #) by Def3;
hence 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G) ; :: thesis: verum