:: deftheorem Def3 defines RealLinearSpace-yielding PRVECT_2:def 3 :
for R being Relation holds
( R is RealLinearSpace-yielding iff for S being set st S in rng R holds
S is RealLinearSpace );