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)

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

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 g + (Carrier LG) or x in Carrier (g + LG) )
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;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

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