let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: 0. G is_a_unity_wrt the addF of G

now

let x be Element of G; :: thesis: ( the addF of G . (0. G),x = x & the addF of G . x,(0. G) = x )
thus the addF of G . (0. G),x = (0. G) + x
.= x by RLVECT_1:10 ; :: thesis: the addF of G . x,(0. G) = x
thus the addF of G . x,(0. G) = x + (0. G)
.= x by RLVECT_1:10 ; :: thesis: verum

end;

hence 0. G is_a_unity_wrt the addF of G by BINOP_1:11; :: thesis: verum