set X = the_set_of_l2ComplexSequences ;
deffunc H₂( set , set ) -> Element of COMPLEX = Sum ((seq_id $1) (#) ((seq_id $2) *' ));
A1: for x, y being set 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 set 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 f being Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :],COMPLEX st
for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
f . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) ; :: thesis: verum