:: deftheorem Def6 defines REAL-US REAL_NS1:def 6 :
for n being Nat
for b₂ being non empty strict UNITSTR holds
( b₂ = REAL-US 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 scalar of b₂ = Euclid_scalar n ) );