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