let RR be domRing; :: thesis: for VV being RightMod of RR
for LL being Linear_Combination of VV
for aa being Scalar of RR st aa <> 0. RR holds
Carrier (LL * aa) = Carrier LL
let VV be RightMod of RR; :: thesis: for LL being Linear_Combination of VV
for aa being Scalar of RR st aa <> 0. RR holds
Carrier (LL * aa) = Carrier LL
let LL be Linear_Combination of VV; :: thesis: for aa being Scalar of RR st aa <> 0. RR holds
Carrier (LL * aa) = Carrier LL
let aa be Scalar of RR; :: thesis: ( aa <> 0. RR implies Carrier (LL * aa) = Carrier LL )
set T = { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } ;
set S = { vv where vv is Vector of VV : LL . vv <> 0. RR } ;
assume A1: aa <> 0. RR ; :: thesis: Carrier (LL * aa) = Carrier LL
{ uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } = { vv where vv is Vector of VV : LL . vv <> 0. RR }

proof

thus { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } c= { vv where vv is Vector of VV : LL . vv <> 0. RR } :: according to XBOOLE_0:def 10 :: thesis: { vv where vv is Vector of VV : LL . vv <> 0. RR } c= { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } or x in { vv where vv is Vector of VV : LL . vv <> 0. RR } )
assume x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } ; :: thesis: x in { vv where vv is Vector of VV : LL . vv <> 0. RR }
then consider uu being Vector of VV such that
A2: x = uu and
A3: (LL * aa) . uu <> 0. RR ;
(LL * aa) . uu = (LL . uu) * aa by Def10;
then LL . uu <> 0. RR by A3;
hence x in { vv where vv is Vector of VV : LL . vv <> 0. RR } by A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { vv where vv is Vector of VV : LL . vv <> 0. RR } or x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } )
assume x in { vv where vv is Vector of VV : LL . vv <> 0. RR } ; :: thesis: x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR }
then consider vv being Vector of VV such that
A4: x = vv and
A5: LL . vv <> 0. RR ;
(LL * aa) . vv = (LL . vv) * aa by Def10;
then (LL * aa) . vv <> 0. RR by A1, A5, VECTSP_2:def 1;
hence x in { uu where uu is Vector of VV : (LL * aa) . uu <> 0. RR } by A4; :: thesis: verum

end;

hence Carrier (LL * aa) = Carrier LL ; :: thesis: verum