let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for LG being Linear_Combination of G holds (0. G) + LG = LG
let LG be Linear_Combination of G; :: thesis: (0. G) + LG = LG

now

let g be Element of G; :: thesis: ((0. G) + LG) . g = LG . g
thus ((0. G) + LG) . g = LG . (g - (0. G)) by Def1
.= LG . g by RLVECT_1:13 ; :: thesis: verum

end;

hence (0. G) + LG = LG by RLVECT_2:def 9; :: thesis: verum