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)

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

hence
g + (LG1 + LG2) = (g + LG1) + (g + LG2)
; :: thesis: verumlet 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;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