:: deftheorem Def4 defines R-normal EUCLID_7:def 4 :
for B0 being set holds
( B0 is R-normal iff for x being real-valued FinSequence st x in B0 holds
|.x.| = 1 );