let R be Relation; :: thesis: ( R is RealLinearSpace-yielding implies R is non-empty-addLoopStr-yielding )
assume R is RealLinearSpace-yielding ; :: thesis: R is non-empty-addLoopStr-yielding
then for x being set st x in rng R holds
x is non empty addLoopStr ;
hence R is non-empty-addLoopStr-yielding by PRVECT_1:def 9; :: thesis: verum