environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SEQ_1, FUNCT_2, TARSKI, REAL_1, BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, CARD_1, NAT_1, RLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, RLSUB_1, REALSET1, SERIES_1, XXREAL_0, SQUARE_1, CARD_3, BHSP_1, COMPLEX1, SEQ_2, ORDINAL2, XXREAL_2, VALUED_0, RSSPACE, ASYMPT_1, FUNCSDOM;
notations HIDDEN, TARSKI, SUBSET_1, XBOOLE_0, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, COMPLEX1, STRUCT_0, ALGSTR_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, REALSET1, FUNCOP_1, RLVECT_1, RLSUB_1, BHSP_1, SQUARE_1, VALUED_1, SEQ_1, SEQ_2, SERIES_1, BINOP_1, FUNCSDOM;
definitions TARSKI, XBOOLE_0, FUNCT_2, RLVECT_1, ALGSTR_0, RLSUB_1;
theorems RELAT_1, TARSKI, ABSVALUE, ZFMISC_1, SEQ_1, SEQ_2, SEQM_3, SERIES_1, COMSEQ_3, INT_1, FUNCT_1, NAT_1, FUNCT_2, RLVECT_1, RLSUB_1, SEQ_4, XREAL_1, ORDINAL1, ALGSTR_0, XREAL_0, FUNCOP_1, FUNCSDOM, VALUED_1;
schemes NAT_1, BINOP_1, XBOOLE_0;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, REALSET1, STRUCT_0, RLVECT_1, BHSP_1, ALGSTR_0, VALUED_1, FUNCT_2, VALUED_0, SERIES_1, SQUARE_1;
constructors HIDDEN, PARTFUN1, BINOP_1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, NAT_D, SEQ_2, SEQM_3, SERIES_1, REALSET1, RLSUB_1, BHSP_1, VALUED_1, RELSET_1, COMSEQ_2, SEQ_1, FUNCSDOM;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SQUARE_1, BINOP_1, RLVECT_1, XBOOLE_0, REALSET1, STRUCT_0, SEQ_1, ALGSTR_0, FUNCSDOM, ORDINAL1;
expansions BINOP_1, RLVECT_1, XBOOLE_0, FUNCSDOM, RLSUB_1;
definition
existence
ex b1 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL st
for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y))
uniqueness
for b1, b2 being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL st ( for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) & ( for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b2 . (x,y) = Sum ((seq_id x) (#) (seq_id y)) ) holds
b1 = b2
end;