environ
vocabularies HIDDEN, FUNCSDOM, VECTSP_1, ARYTM_1, SUPINF_2, STRUCT_0, RLVECT_1, ALGSTR_0, XBOOLE_0, MESFUNC1, VECTSP_2, RLVECT_2, FINSEQ_1, FINSET_1, SUBSET_1, TARSKI, FUNCT_1, RELAT_1, CARD_3, VALUED_1, ARYTM_3, RLVECT_3, RLSUB_1, FUNCT_2, PRELAMB, ZFMISC_1, ORDINAL1, ORDERS_1, MOD_3;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FINSET_1, FINSEQ_1, RELAT_1, FUNCT_1, ORDERS_1, DOMAIN_1, STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_2, GROUP_1, RLVECT_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7;
definitions XBOOLE_0, TARSKI, VECTSP_4, VECTSP_6, VECTSP_7;
theorems FINSET_1, FUNCT_1, ORDERS_1, RLVECT_3, SUBSET_1, TARSKI, VECTSP_1, VECTSP_2, ZFMISC_1, RLVECT_1, VECTSP_4, VECTSP_6, FUNCT_2, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, RLSUB_2, CARD_2, STRUCT_0, VECTSP_7;
schemes FUNCT_1, FUNCT_2, XFAMILY;
registrations SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_2, VECTSP_4, ORDINAL1, VECTSP_7;
constructors HIDDEN, ORDERS_1, PARTFUN1, REALSET1, VECTSP_5, VECTSP_6, RELSET_1, VECTSP_7, GROUP_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities XBOOLE_0, VECTSP_4, VECTSP_6, VECTSP_7;
expansions XBOOLE_0, TARSKI, VECTSP_7;
Lm1:
for R being Ring
for a being Scalar of R st - a = 0. R holds
a = 0. R
Lm2:
for R being Skew-Field
for a being Scalar of R
for V being LeftMod of R
for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
Lm3:
for R being non degenerated almost_left_invertible Ring
for V being LeftMod of R ex B being Subset of V st B is base