environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, NAT_1, BINOP_1, FUNCT_1, ARYTM_3, FINSEQ_2, ZFMISC_1, RELAT_1, COMPLEX1, STRUCT_0, XBOOLE_0, NORMSP_1, SUPINF_2, EUCLID, ALGSTR_0, RLVECT_1, PRE_TOPC, REAL_1, CARD_1, XXREAL_0, ARYTM_1, FINSEQ_1, CARD_3, ORDINAL4, TARSKI, RVSUM_1, SQUARE_1, SEQ_2, ORDINAL2, SEQ_1, VALUED_1, RSSPACE3, LOPBAN_1, REWRITE1, BHSP_1, PROB_2, BINOP_2, METRIC_1, BHSP_3, REAL_NS1, RELAT_2, NORMSP_0, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, BINOP_1, PRE_TOPC, ORDINAL1, XCMPLX_0, NAT_1, FINSEQ_1, FINSEQ_2, FUNCT_2, STRUCT_0, ALGSTR_0, FUNCOP_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, COMPLEX1, REAL_1, RLVECT_1, BHSP_1, BHSP_2, BINOP_2, VALUED_1, SEQ_1, SEQ_2, RVSUM_1, NORMSP_0, NORMSP_1, EUCLID, RSSPACE3, LOPBAN_1, BHSP_3;
definitions RLVECT_1, RSSPACE3, BHSP_3, ALGSTR_0, NORMSP_0;
theorems XREAL_0, NORMSP_1, EUCLID, RLVECT_1, SEQ_2, SEQ_4, BINOP_1, COMPLEX1, ABSVALUE, RSSPACE3, FINSEQ_1, FINSEQ_2, RVSUM_1, FUNCT_2, LOPBAN_1, ZFMISC_1, FUNCOP_1, SEQ_1, NAT_1, SQUARE_1, FUNCT_1, FINSEQ_5, XREAL_1, RFUNCT_4, BHSP_2, EUCLID_2, EUCLID_4, EUCLIDLP, XXREAL_0, VALUED_1, NORMSP_0, ORDINAL1, CARD_1;
schemes NAT_1, SEQ_1, BINOP_1, BINOP_2, FUNCT_2, FINSEQ_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_2, STRUCT_0, NORMSP_0, NORMSP_1, BHSP_1, REVROT_1, RSSPACE3, VALUED_0, VALUED_1, FUNCT_2, EUCLID, FINSEQ_1, CARD_1, SQUARE_1, RVSUM_1, NAT_1;
constructors HIDDEN, REAL_1, SQUARE_1, BINOP_2, COMPLEX1, SEQ_2, FINSEQOP, REALSET2, BHSP_2, BHSP_3, RSSPACE3, LOPBAN_1, RVSUM_1, EUCLID, RELSET_1, COMSEQ_2, BINOP_1;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RLVECT_1, BINOP_1, BHSP_1, RSSPACE3, SQUARE_1, STRUCT_0, ALGSTR_0, VALUED_1, NORMSP_0;
expansions RLVECT_1, BINOP_1, BHSP_1, RSSPACE3, BHSP_3, NORMSP_0;
Lm1:
for n being Nat ex ADD being BinOp of (REAL n) st
( ( for a, b being Element of REAL n holds ADD . (a,b) = a + b ) & ADD is commutative & ADD is associative )
Lm2:
for n being Nat holds REAL-NS n is RealBanachSpace
definition
let n be
Nat;
existence
ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y))
uniqueness
for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = Sum (mlt (x,y)) ) & ( for x, y being Element of REAL n holds b2 . (x,y) = Sum (mlt (x,y)) ) holds
b1 = b2
end;