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