let c be XFinSequence of REAL ; :: thesis: for a being Real holds a (#) c is XFinSequence of REAL
let a be Real; :: thesis: a (#) c is XFinSequence of REAL
dom (a (#) c) = dom c by VALUED_1:def 5;
then a (#) c is Sequence of rng (a (#) c) by ORDINAL1:31;
hence a (#) c is XFinSequence of REAL by ORDINAL1:32; :: thesis: verum