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 :: thesis: for g being Element of G holds ((0. G) + LG) . g = LG . g

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 ; :: thesis: verum

end;

hence (0. G) + LG = LG ; :: thesis: verum