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 object 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 object 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
A2: for x, y being object 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
A3: for x, y being object 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 A4: ( 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 A2, A4
.= scalar2 . (x,y) by A3, A4 ; :: thesis: verum
end;
hence scalar1 = scalar2 ; :: thesis: verum