deffunc H2( object , object ) -> Element of COMPLEX = Sum ((seq_id $1) (#) ((seq_id $2) *'));
set X = the_set_of_l2ComplexSequences ;
A1:
for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
H2(x,y) in COMPLEX
;
ex f being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX st
for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
f . (x,y) = H2(x,y)
from BINOP_1:sch 2(A1);
hence
ex b1 being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX st
for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b1 . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *'))
; verum