set X = the_set_of_l2RealSequences ;
let scalar1, scalar2 be Function of ,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 (() (#) ()) ) & ( for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
scalar2 . (x,y) = Sum (() (#) ()) ) 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 (() (#) ()) 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 (() (#) ()) ; :: 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 (() (#) ()) by A2, A4
.= scalar2 . (x,y) by A3, A4 ; :: thesis: verum
end;
hence scalar1 = scalar2 ; :: thesis: verum