environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, PARTFUN1, FUNCT_1, TARSKI, RELAT_1, SUPINF_1, XXREAL_0, ORDINAL1, ARYTM_3, ORDINAL2, XXREAL_2, RLVECT_1, RLSUB_1, STRUCT_0, SUPINF_2, RLSUB_2, FINSEQ_4, MCART_1, RLVECT_3, REAL_1, CARD_1, MSSUBFAM, UNIALG_1, COMPLEX1, FUNCOP_1, ARYTM_1, ALGSTR_0, REALSET1, ZFMISC_1, NORMSP_1, HAHNBAN, NORMSP_0, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, RLVECT_1, RLSUB_1, RLSUB_2, NORMSP_0, NORMSP_1, SUPINF_1, PARTFUN1, FUNCOP_1, RLVECT_3, DOMAIN_1, XXREAL_2;
definitions TARSKI, RLSUB_1, RLSUB_2, RLVECT_1, ORDINAL1, XBOOLE_0, ALGSTR_0, XXREAL_2;
theorems PARTFUN1, RLSUB_1, FUNCT_2, ZFMISC_1, FUNCOP_1, TREES_2, TARSKI, FUNCT_1, GRFUNC_1, RLVECT_1, RLSUB_2, RLVECT_4, MCART_1, RLVECT_3, ABSVALUE, NORMSP_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, NUMBERS, XXREAL_2, NORMSP_0, XREAL_0;
schemes ORDERS_1, DOMAIN_1, FUNCT_2;
registrations SUBSET_1, RELSET_1, PARTFUN1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, RLVECT_1, RLSUB_1, ALGSTR_0, FUNCT_2, FUNCT_1, RELAT_1, ORDINAL1, XTUPLE_0;
constructors HIDDEN, BINOP_1, REAL_1, COMPLEX1, SUPINF_1, REALSET1, RFUNCT_3, RLSUB_2, RLVECT_2, RLVECT_3, NORMSP_1, XXREAL_2, RELSET_1, XXREAL_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities RLVECT_1, XBOOLE_0, STRUCT_0, ALGSTR_0, RLSUB_1;
expansions TARSKI, XBOOLE_0, STRUCT_0;
Lm1:
for V being RealLinearSpace
for X being Subspace of V
for v being VECTOR of V st not v in the carrier of X holds
for q being Banach-Functional of V
for fi being linear-Functional of X st ( for x being VECTOR of X
for v being VECTOR of V st x = v holds
fi . x <= q . v ) holds
ex psi being linear-Functional of (X + (Lin {v})) st
( psi | the carrier of X = fi & ( for x being VECTOR of (X + (Lin {v}))
for v being VECTOR of V st x = v holds
psi . x <= q . v ) )
Lm2:
for V being RealLinearSpace holds RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) is RealLinearSpace
Lm3:
for V, V9, W9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for W being Subspace of V st W9 = RLSStruct(# the carrier of W, the ZeroF of W, the addF of W, the Mult of W #) holds
W9 is Subspace of V9
Lm4:
for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for f being linear-Functional of V9 holds f is linear-Functional of V
Lm5:
for V, V9 being RealLinearSpace st V9 = RLSStruct(# the carrier of V, the ZeroF of V, the addF of V, the Mult of V #) holds
for f being linear-Functional of V holds f is linear-Functional of V9