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;
now :: thesis: for r being Real st r in rng (a (#) c) holds
0 < r
let r be Real; :: thesis: ( r in rng (a (#) c) implies 0 < r )
assume r in rng (a (#) c) ; :: thesis: 0 < r
then consider x being object such that
P4: ( x in dom (a (#) c) & r = (a (#) c) . x ) by FUNCT_1:def 3;
c . x in rng c by FUNCT_1:3, P4, P2;
then P5: 0 < c . x by PARTFUN3:def 1;
r = a * (c . x) by P4, VALUED_1:6;
hence 0 < r by P5, AS; :: thesis: verum
end;
then a (#) c is positive-yielding ;
hence a (#) c is non empty positive-yielding XFinSequence of REAL by NLM1, P2; :: thesis: verum