for RR being domRing
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