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

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 Def5 ; :: thesis: the multF of G . h,(1_ G) = h
thus the multF of G . h,(1_ G) = h * (1_ G)
.= h by Def5 ; :: thesis: verum

end;

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