environ
vocabularies HIDDEN, RLSUB_1, HAHNBAN, UNIALG_1, DUALSP01, DUALSP02, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, RSSPACE3, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, FUNCOP_1, FCONT_1, NORMSP_0, SEQ_2, LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, PRE_TOPC, SUBSET_1, ZFMISC_1, NUMBERS, SEQ_4, XBOOLE_0, CARD_1, SUPINF_2, COMPLEX1, XXREAL_0, XXREAL_2, NAT_1, REWRITE1, METRIC_1, RELAT_2, FUNCT_7, RCOMP_1, NORMSP_2, RLVECT_3, BINOP_2, NORMSP_3, EUCLID, MOD_4, MEMBERED;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, EUCLID, FUNCT_2, BINOP_1, BINOP_2, DOMAIN_1, FUNCOP_1, NUMBERS, MEMBERED, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, COMPLEX1, XXREAL_2, SEQ_4, STRUCT_0, ALGSTR_0, PRE_TOPC, RLVECT_1, RLVECT_3, RLSUB_1, VECTSP_1, NORMSP_0, NORMSP_1, NORMSP_2, HAHNBAN, RSSPACE, RSSPACE3, LOPBAN_1, NFCONT_1, DUALSP01, NORMSP_3;
definitions ALGSTR_0, RLVECT_1, VECTSP_1, HAHNBAN, LOPBAN_1, TARSKI;
theorems SEQ_4, FUNCT_1, ABSVALUE, COMPLEX1, TARSKI, RSSPACE3, XREAL_0, XXREAL_0, NORMSP_1, LOPBAN_1, FUNCT_2, XBOOLE_0, XREAL_1, RLVECT_1, FUNCOP_1, VECTSP_1, HAHNBAN, RLSUB_1, NORMSP_0, ORDINAL1, NORMSP_3, SUBSET_1, ZFMISC_1, XXREAL_2, DUALSP01, RELAT_1, XCMPLX_1, NORMSP_2, BINOP_2, LOPBAN_5, RLVECT_4, EUCLID;
schemes FUNCT_2;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, XXREAL_0, VALUED_0, RLVECT_1, FUNCT_2, SEQ_4, RELSET_1, FUNCT_1, NORMSP_3, NORMSP_0, NORMSP_1, DUALSP01, XBOOLE_0, LOPBAN_1;
constructors HIDDEN, REAL_1, EUCLID, REALSET1, RSSPACE3, BINOP_2, RELSET_1, SEQ_4, HAHNBAN1, NORMSP_2, PCOMPS_1, RLVECT_3, NORMSP_3, NFCONT_1, MEMBERED;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities RLVECT_1, STRUCT_0, ALGSTR_0, NORMSP_0, FUNCSDOM, NORMSP_3, PCOMPS_1, DUALSP01, NORMSP_2, SEQ_4;
expansions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, FUNCT_2, NORMSP_0, NORMSP_1, VECTSP_1, STRUCT_0, RLVECT_1, NORMSP_3, XXREAL_2, MEMBERED, DUALSP01;
LMNORM:
for X being RealNormSpace
for x being Point of X st not X is trivial holds
||.x.|| = ||.((BidualFunc X) . x).||
NISOM11:
for X, Y being RealNormSpace st ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism & X is Reflexive holds
Y is Reflexive
Lm77R:
for X being RealBanachSpace st not X is trivial & X is Reflexive holds
DualSp X is Reflexive