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

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