:: deftheorem Def2 defines Basis RUSUB_3:def 2 :
for V being RealUnitarySpace
for b₂ being Subset of V holds
( b₂ is Basis of V iff ( b₂ is linearly-independent & Lin b₂ = UNITSTR(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V, the scalar of V #) ) );