environ
vocabularies HIDDEN, BHSP_1, SUBSET_1, RLVECT_3, STRUCT_0, RLSUB_1, CARD_3, RLVECT_2, TARSKI, RLVECT_1, ARYTM_3, REAL_1, RELAT_1, SUPINF_2, CARD_1, FUNCT_1, NUMBERS, FUNCT_2, FINSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, ORDERS_1, ARYTM_1, FINSEQ_1, VALUED_1, NAT_1, ORDINAL4, CLASSES1, XXREAL_0, PARTFUN1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, ORDERS_1, DOMAIN_1, STRUCT_0, RLVECT_1, FINSET_1, RLSUB_1, RLVECT_2, BHSP_1, RLVECT_3, RUSUB_1, RUSUB_2, CLASSES1, XXREAL_0;
definitions XBOOLE_0, RLVECT_2, TARSKI, RLVECT_3, RLSUB_1;
theorems FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSET_1, ORDERS_1, RLSUB_2, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, RUSUB_1, RUSUB_2, RLVECT_3, ENUMSET1, RLVECT_4, RFINSEQ, NAT_1, SUBSET_1, XCMPLX_0, XCMPLX_1, CARD_2, STRUCT_0, PARTFUN1, XREAL_0;
schemes FUNCT_1, FUNCT_2, NAT_1, RLVECT_4, XFAMILY;
registrations SUBSET_1, ORDINAL1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, FINSEQ_1, STRUCT_0, RLVECT_3, BHSP_1, RUSUB_1, CARD_1, RLVECT_2, XREAL_0;
constructors HIDDEN, PARTFUN1, XXREAL_0, REAL_1, NAT_1, ORDERS_1, REALSET1, RFINSEQ, RLVECT_2, RLVECT_3, CLASSES1, RUSUB_2, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, RLVECT_2, RLVECT_1;
expansions XBOOLE_0, TARSKI, RLVECT_3;
reconsider jj = 1, zz = In (0,REAL) as Element of REAL by XREAL_0:def 1;
Lm1:
for V being RealUnitarySpace
for x being object holds
( x in (0). V iff x = 0. V )
Lm2:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
Lm3:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 & W1 is Subspace of W3 holds
W1 is Subspace of W2 /\ W3
Lm4:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
Lm5:
for V being RealUnitarySpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 & W2 is Subspace of W3 holds
W1 + W2 is Subspace of W3
Lm6:
for X, x being set st not x in X holds
X \ {x} = X