set X = the_set_of_l2ComplexSequences ;
let scalar1, scalar2 be Function of [:the_set_of_l2ComplexSequences ,the_set_of_l2ComplexSequences :],COMPLEX ; :: thesis: ( ( for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
scalar1 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) ) & ( for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
scalar2 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) ) implies scalar1 = scalar2 )
assume that
A1: for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
scalar1 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) and
A2: for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
scalar2 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) ; :: thesis: scalar1 = scalar2
for x, y being set st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
scalar1 . x,y = scalar2 . x,y

proof

let x, y be set ; :: thesis: ( x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences implies scalar1 . x,y = scalar2 . x,y )
assume that
A3: x in the_set_of_l2ComplexSequences and
A4: y in the_set_of_l2ComplexSequences ; :: thesis: scalar1 . x,y = scalar2 . x,y
thus scalar1 . x,y = Sum ((seq_id x) (#) ((seq_id y) *' )) by A1, A3, A4
.= scalar2 . x,y by A2, A3, A4 ; :: thesis: verum

end;

hence scalar1 = scalar2 by BINOP_1:1; :: thesis: verum