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 object 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 object 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
A2: for x, y being object 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
A3: for x, y being object 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
A4: x in the_set_of_l2ComplexSequences and
A5: 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 A2, A4, A5
.= scalar2 . (x,y) by A3, A4, A5 ; :: thesis: verum

end;

hence scalar1 = scalar2 ; :: thesis: verum