:: deftheorem defines l_scalar RSSPACE:def 12 :
for b₁ being Function of [:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL holds
( b₁ = l_scalar iff for x, y being object st x in the_set_of_l2RealSequences & y in the_set_of_l2RealSequences holds
b₁ . (x,y) = Sum ((seq_id x) (#) (seq_id y)) );