environ
vocabularies HIDDEN, VECTSP_1, SUBSET_1, FINSET_1, RLVECT_2, FUNCT_1, STRUCT_0, RLVECT_3, CARD_3, SUPINF_2, XBOOLE_0, TARSKI, GROUP_1, FUNCT_2, RELAT_1, ARYTM_1, ARYTM_3, MESFUNC1, RLSUB_1, ZFMISC_1, ORDINAL1, ORDERS_1, RLVECT_1, ALGSTR_0, BINOP_1, LATTICES, FUNCSDOM, FINSEQ_1, VECTSP_2, MOD_3, PRELAMB, VALUED_1, PARTFUN1, ORDINAL4, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCT_2, FINSET_1, ORDERS_1, DOMAIN_1, STRUCT_0, ORDINAL1, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6;
definitions XBOOLE_0, VECTSP_4, VECTSP_6, TARSKI;
theorems FUNCT_1, FINSET_1, ORDERS_1, RLVECT_3, TARSKI, VECTSP_1, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, ZFMISC_1, RLVECT_1, FUNCT_2, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, CARD_2, STRUCT_0, PARTFUN1, RLVECT_2, SUBSET_1, FINSEQ_1, FINSEQ_3, FINSEQ_4;
schemes FUNCT_1, FUNCT_2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, VECTSP_1, VECTSP_4, ALGSTR_0, VECTSP_2, ORDINAL1;
constructors HIDDEN, ORDERS_1, REALSET1, VECTSP_5, VECTSP_6, STRUCT_0, GROUP_1, RLVECT_2, VECTSP_2, PARTFUN1, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities VECTSP_4, VECTSP_6, XBOOLE_0;
expansions XBOOLE_0, TARSKI;
TH2:
for GF being Ring
for V being LeftMod of GF
for L being Linear_Combination of V
for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
TH3:
for GF being Ring
for V being LeftMod of GF
for L being Linear_Combination of V
for a being Scalar of holds Sum (a * L) = a * (Sum L)
Lm1:
for R being Ring
for a being Scalar of R st - a = 0. R holds
a = 0. R
Lm2:
for R being non degenerated almost_left_invertible Ring
for V being LeftMod of R
for a being Scalar of
for v being Vector of V st a <> 0. R holds
( (a ") * (a * v) = (1. R) * v & ((a ") * a) * v = (1. R) * v )
Lem0A:
for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being LeftMod of GF holds {} the carrier of V is linearly-independent
Lem1A:
for GF being non empty right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for V being LeftMod of GF holds (0). V is free