deffunc H₁( set , set ) -> Element of REAL = Sum ((seq_id $1) (#) (seq_id $2));
set X = the_set_of_l2RealSequences ;
A1: for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
H₁(x,y) in REAL ;
ex f being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :],REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
f . x,y = H₁(x,y) from BINOP_1:sch 2(A1);
hence ex f being Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :],REAL st
for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
f . x,y = Sum ((seq_id x) (#) (seq_id y)) ; :: thesis: verum