let G be non empty add-unital addMagma ; :: thesis: 0_ G is_a_unity_wrt the addF of G
set o = the addF of G;

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

let h be Element of G; :: thesis: ( the addF of G . ((0_ G),h) = h & the addF of G . (h,(0_ G)) = h )
thus the addF of G . ((0_ G),h) = (0_ G) + h
.= h by Def4 ; :: thesis: the addF of G . (h,(0_ G)) = h
thus the addF of G . (h,(0_ G)) = h + (0_ G)
.= h by Def4 ; :: thesis: verum

end;

hence 0_ G is_a_unity_wrt the addF of G by BINOP_1:3; :: thesis: verum