deffunc H₂( 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
H₂(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) = H₂(x,y) from BINOP_1:sch 2(A1);
hence ex b₁ 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
b₁ . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) ; :: thesis: verum