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