:: deftheorem defines cl_scalar CSSPACE:def 17 :
for b₁ being Function of [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:],COMPLEX holds
( b₁ = cl_scalar iff for x, y being object st x in the_set_of_l2ComplexSequences & y in the_set_of_l2ComplexSequences holds
b₁ . (x,y) = Sum ((seq_id x) (#) ((seq_id y) *')) );