deffunc H1( object , object ) -> object = Sum ((seq_id $1) (#) (seq_id $2));
set X = the_set_of_l2RealSequences ;
A1:
for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
H1(x,y) in REAL
by XREAL_0:def 1;
ex f 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
f . (x,y) = H1(x,y)
from BINOP_1:sch 2(A1);
hence
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))
; verum