let R be Ring; :: thesis: for V being RightMod of R
for L being Linear_Combination of V holds Carrier (- L) = Carrier L
let V be RightMod of R; :: thesis: for L being Linear_Combination of V holds Carrier (- L) = Carrier L
let L be Linear_Combination of V; :: thesis: Carrier (- L) = Carrier L
set a = - (1_ R);
Carrier (L * (- (1_ R))) = Carrier L

proof

set S = { v where v is Vector of V : L . v <> 0. R } ;
set T = { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } ;
{ u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } = { v where v is Vector of V : L . v <> 0. R }

proof

thus { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } c= { v where v is Vector of V : L . v <> 0. R } :: according to XBOOLE_0:def 10 :: thesis: { v where v is Vector of V : L . v <> 0. R } c= { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } or x in { v where v is Vector of V : L . v <> 0. R } )
assume x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } ; :: thesis: x in { v where v is Vector of V : L . v <> 0. R }
then consider u being Vector of V such that
A1: x = u and
A2: (L * (- (1_ R))) . u <> 0. R ;
(L * (- (1_ R))) . u = (L . u) * (- (1_ R)) by Def10;
then L . u <> 0. R by A2;
hence x in { v where v is Vector of V : L . v <> 0. R } by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Vector of V : L . v <> 0. R } or x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } )
assume x in { v where v is Vector of V : L . v <> 0. R } ; :: thesis: x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R }
then consider v being Vector of V such that
A3: x = v and
A4: L . v <> 0. R ;
(L * (- (1_ R))) . v = (L . v) * (- (1_ R)) by Def10
.= - (L . v) by VECTSP_2:28 ;
then (L * (- (1_ R))) . v <> 0. R by A4, VECTSP_2:3;
hence x in { u where u is Vector of V : (L * (- (1_ R))) . u <> 0. R } by A3; :: thesis: verum

end;

hence Carrier (L * (- (1_ R))) = Carrier L ; :: thesis: verum

end;

hence Carrier (- L) = Carrier L ; :: thesis: verum