:: deftheorem Def2 defines Complex_linfty_norm CSSPACE4:def 2 :
for b₁ being Function of the_set_of_BoundedComplexSequences,REAL holds
( b₁ = Complex_linfty_norm iff for x being object st x in the_set_of_BoundedComplexSequences holds
b₁ . x = upper_bound (rng |.(seq_id x).|) );