let G be non empty unital multMagma ; :: thesis: 1_ G is_a_unity_wrt the multF of G
set o = the multF of G;

now :: thesis: for h being Element of G holds
( the multF of G . ((1_ G),h) = h & the multF of G . (h,(1_ G)) = h )

let h be Element of G; :: thesis: ( the multF of G . ((1_ G),h) = h & the multF of G . (h,(1_ G)) = h )
thus the multF of G . ((1_ G),h) = (1_ G) * h
.= h by Def4 ; :: thesis: the multF of G . (h,(1_ G)) = h
thus the multF of G . (h,(1_ G)) = h * (1_ G)
.= h by Def4 ; :: thesis: verum

end;

hence 1_ G is_a_unity_wrt the multF of G by BINOP_1:3; :: thesis: verum