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

hence 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G) ; :: thesis: verum

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

hence 1. (.: (G,X)) = X --> (the_unity_wrt the multF of G) ; :: thesis: verum