environ
vocabularies HIDDEN, FUNCSDOM, VECTSP_1, VECTSP_2, SUBSET_1, RLSUB_1, ARYTM_3, RELAT_1, XBOOLE_0, SUPINF_2, ARYTM_1, GROUP_1, STRUCT_0, TARSKI, ALGSTR_0, ZFMISC_1, FUNCT_1, REALSET1, RLVECT_1, BINOP_1, RMOD_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, REALSET1, STRUCT_0, ALGSTR_0, DOMAIN_1, RLVECT_1, BINOP_1, GROUP_1, VECTSP_1, VECTSP_2;
definitions TARSKI, VECTSP_2, RLVECT_1, XBOOLE_0, ALGSTR_0;
theorems FUNCT_1, FUNCT_2, TARSKI, VECTSP_1, ZFMISC_1, VECTSP_2, RLVECT_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, ALGSTR_0;
schemes XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, REALSET1, STRUCT_0, VECTSP_1, VECTSP_2, RELAT_1, ALGSTR_0;
constructors HIDDEN, PARTFUN1, BINOP_1, REALSET1, VECTSP_2, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities VECTSP_2, BINOP_1, REALSET1, STRUCT_0, ALGSTR_0;
expansions TARSKI, XBOOLE_0, STRUCT_0;
Lm1:
for R being Ring
for V being RightMod of R
for V1 being Subset of V
for W being Submodule of V st the carrier of W = V1 holds
V1 is linearly-closed
Lm2:
for R being Ring
for V being RightMod of R
for W being Submodule of V holds (0. V) + W = the carrier of W
Lm3:
for R being Ring
for V being RightMod of R
for v being Vector of V
for W being Submodule of V holds
( v in W iff v + W = the carrier of W )