:: deftheorem Def10 defines RealNormSpace-yielding PRVECT_2:def 10 :
for R being Relation holds
( R is RealNormSpace-yielding iff for x being set st x in rng R holds
x is RealNormSpace );