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

now :: thesis: for s being Element of G holds (g + (h + LG)) . s = ((g + h) + LG) . s

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

end;

hence g + (h + LG) = (g + h) + LG ; :: thesis: verum