let G be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for LG being Linear_Combination of G
for g being Element of G holds Carrier (g + LG) = g + (Carrier LG)
let LG be Linear_Combination of G; :: thesis: for g being Element of G holds Carrier (g + LG) = g + (Carrier LG)
let g be Element of G; :: thesis: Carrier (g + LG) = g + (Carrier LG)
thus Carrier (g + LG) c= g + (Carrier LG) :: according to XBOOLE_0:def 10 :: thesis: g + (Carrier LG) c= Carrier (g + LG)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier (g + LG) or x in g + (Carrier LG) )
assume A1: x in Carrier (g + LG) ; :: thesis: x in g + (Carrier LG)
reconsider w = x as Element of G by A1;
A2: (g + LG) . w <> 0 by A1, RLVECT_2:19;
A3: g + (w - g) = (w + (- g)) + g by RLVECT_1:def 11
.= w + (g + (- g)) by RLVECT_1:def 3
.= w + (0. G) by RLVECT_1:def 10
.= w ;
(g + LG) . w = LG . (w - g) by Def1;
then w - g in Carrier LG by A2;
hence x in g + (Carrier LG) by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g + (Carrier LG) or x in Carrier (g + LG) )
assume x in g + (Carrier LG) ; :: thesis: x in Carrier (g + LG)
then consider w being Element of G such that
A4: x = g + w and
A5: w in Carrier LG ;
(g + w) - g = (g + w) + (- g) by RLVECT_1:def 11
.= ((- g) + g) + w by RLVECT_1:def 3
.= (0. G) + w by RLVECT_1:5
.= w ;
then A6: (g + LG) . (g + w) = LG . w by Def1;
LG . w <> 0 by A5, RLVECT_2:19;
hence x in Carrier (g + LG) by A4, A6; :: thesis: verum