:: deftheorem Def4 defines REAL-NS REAL_NS1:def 4 :
for n being Nat
for b₂ being non empty strict NORMSTR holds
( b₂ = REAL-NS n iff ( the carrier of b₂ = REAL n & 0. b₂ = 0* n & the addF of b₂ = Euclid_add n & the Mult of b₂ = Euclid_mult n & the normF of b₂ = Euclid_norm n ) );