:: deftheorem Def2 defines linfty_norm RSSPACE4:def 2 :
for b₁ being Function of the_set_of_BoundedRealSequences,REAL holds
( b₁ = linfty_norm iff for x being object st x in the_set_of_BoundedRealSequences holds
b₁ . x = upper_bound (rng (abs (seq_id x))) );