environ
vocabularies HIDDEN, REAL_1, SUBSET_1, NUMBERS, RLVECT_1, RLSUB_1, FINSET_1, RLVECT_2, FINSEQ_1, STRUCT_0, FUNCT_1, XBOOLE_0, ORDERS_1, VALUED_1, ORDINAL4, ARYTM_3, RELAT_1, PARTFUN1, NAT_1, CARD_3, CARD_1, SUPINF_2, FINSEQ_4, TARSKI, FUNCT_2, ARYTM_1, ZFMISC_1, ORDINAL1, RLVECT_3, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, FINSEQ_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, ORDERS_1, DOMAIN_1, XCMPLX_0, XREAL_0, STRUCT_0, RLVECT_1, FINSEQ_4, FINSET_1, REAL_1, RLSUB_1, RLSUB_2, RLVECT_2, NAT_1;
definitions XBOOLE_0, RLSUB_1, RLVECT_2, TARSKI;
theorems CARD_2, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSET_1, RLSUB_1, RLSUB_2, RLVECT_1, RLVECT_2, TARSKI, ZFMISC_1, RELAT_1, ORDINAL1, XBOOLE_0, XBOOLE_1, XCMPLX_0, ORDERS_1, STRUCT_0, PARTFUN1, XREAL_0;
schemes FINSEQ_1, FUNCT_1, FUNCT_2, XFAMILY;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, NUMBERS, STRUCT_0, RLVECT_1, RLSUB_1, ORDINAL1, XREAL_0, RLVECT_2;
constructors HIDDEN, PARTFUN1, REAL_1, NAT_1, ORDERS_1, FINSEQ_4, REALSET1, RLSUB_2, RLVECT_2, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RLSUB_1, RLVECT_2;
expansions XBOOLE_0, TARSKI;
Lm1:
for V being RealLinearSpace
for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm2:
for x being object
for V being RealLinearSpace holds
( x in (0). V iff x = 0. V )
Lm3:
for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W3 holds
W1 /\ W2 is Subspace of W3
Lm4:
for V being RealLinearSpace
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
Lm5:
for V being RealLinearSpace
for W1, W2, W3 being Subspace of V st W1 is Subspace of W2 holds
W1 is Subspace of W2 + W3
Lm6:
for V being RealLinearSpace
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
Lm7:
for M being non empty set
for CF being Choice_Function of M st not {} in M holds
dom CF = M
:: Auxiliary theorems.
::