set X = the_set_of_l2ComplexSequences ;
let scalar1, scalar2 be Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX; ( ( 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) *'))
; 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 ;
( 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
;
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
;
verum
end;
hence
scalar1 = scalar2
; verum