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 :: thesis: for x being Element of G holds

( the addF of G . ((0. G),x) = x & the addF of G . (x,(0. G)) = x )

hence
0. G is_a_unity_wrt the addF of G
by BINOP_1:3; :: thesis: verum( the addF of G . ((0. G),x) = x & the addF of G . (x,(0. G)) = x )

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:4 ; :: thesis: the addF of G . (x,(0. G)) = x

thus the addF of G . (x,(0. G)) = x + (0. G)

.= x by RLVECT_1:4 ; :: thesis: verum

end;thus the addF of G . ((0. G),x) = (0. G) + x

.= x by RLVECT_1:4 ; :: thesis: the addF of G . (x,(0. G)) = x

thus the addF of G . (x,(0. G)) = x + (0. G)

.= x by RLVECT_1:4 ; :: thesis: verum