let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for g being Element of G holds g + (ZeroLC G) = ZeroLC G
let g be Element of G; :: thesis: g + (ZeroLC G) = ZeroLC G
Carrier (ZeroLC G) = {} G by RLVECT_2:def 5;
then {} G = g + (Carrier (ZeroLC G)) by Th8
.= Carrier (g + (ZeroLC G)) by Th16 ;
hence g + (ZeroLC G) = ZeroLC G by RLVECT_2:def 5; :: thesis: verum