environ
vocabularies HIDDEN, RLVECT_1, REAL_1, SUBSET_1, ARYTM_3, RELAT_1, XBOOLE_0, SUPINF_2, CARD_1, ARYTM_1, STRUCT_0, TARSKI, ALGSTR_0, REALSET1, ZFMISC_1, NUMBERS, FUNCT_1, BINOP_1, RLSUB_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, REALSET1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1;
definitions RLVECT_1, TARSKI, XBOOLE_0, ALGSTR_0;
theorems FUNCT_1, FUNCT_2, RLVECT_1, TARSKI, ZFMISC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, STRUCT_0, ALGSTR_0, XREAL_0;
schemes XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, NUMBERS, REALSET1, STRUCT_0, RLVECT_1, ORDINAL1, ALGSTR_0, XREAL_0;
constructors HIDDEN, PARTFUN1, BINOP_1, REAL_1, NAT_1, REALSET1, RLVECT_1, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RLVECT_1, REALSET1, BINOP_1, STRUCT_0, ALGSTR_0;
expansions TARSKI, XBOOLE_0, STRUCT_0;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm1:
for V being RealLinearSpace
for V1 being Subset of V
for W being Subspace of V st the carrier of W = V1 holds
V1 is linearly-closed
Lm2:
for V being RealLinearSpace
for W being Subspace of V holds (0. V) + W = the carrier of W
Lm3:
for V being RealLinearSpace
for v being VECTOR of V
for W being Subspace of V holds
( v in W iff v + W = the carrier of W )
:: Introduction of predicate linearly closed subsets of the carrier.
::