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