let c be non empty positive-yielding XFinSequence of REAL ; :: thesis: for a being Real st 0 < a holds
a (#) c is non empty positive-yielding XFinSequence of REAL
let a be Real; :: thesis: ( 0 < a implies a (#) c is non empty positive-yielding XFinSequence of REAL )
assume AS: 0 < a ; :: thesis: a (#) c is non empty positive-yielding XFinSequence of REAL
P2: dom (a (#) c) = dom c by VALUED_1:def 5;
for r being Real st r in rng (a (#) c) holds
0 < r by PARTFUN3:def 1, AS;
then a (#) c is positive-yielding ;
hence a (#) c is non empty positive-yielding XFinSequence of REAL by P2; :: thesis: verum