set X = the_set_of_l2RealSequences ;
let scalar1, scalar2 be Function of [:the_set_of_l2RealSequences ,the_set_of_l2RealSequences :],REAL ; :: thesis: ( ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar1 . x,y = Sum ((seq_id x) (#) (seq_id y)) ) & ( for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences 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_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar1 . x,y = Sum ((seq_id x) (#) (seq_id y)) and
A2: for x, y being set st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences 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_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar1 . x,y = scalar2 . x,y

proof

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

end;

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