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

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

let h be Element of G; :: thesis: (g + (LG1 + LG2)) . h = ((g + LG1) + (g + LG2)) . h
thus (g + (LG1 + LG2)) . h = (LG1 + LG2) . (h - g) by Def1
.= (LG1 . (h - g)) + (LG2 . (h - g)) by RLVECT_2:def 10
.= ((g + LG1) . h) + (LG2 . (h - g)) by Def1
.= ((g + LG1) . h) + ((g + LG2) . h) by Def1
.= ((g + LG1) + (g + LG2)) . h by RLVECT_2:def 10 ; :: thesis: verum

end;

hence g + (LG1 + LG2) = (g + LG1) + (g + LG2) ; :: thesis: verum