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

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