let D be non empty set ; :: thesis: for T being FinSequence of D
for f being Function of D,NAT holds f * T is FinSequence of REAL
let T be FinSequence of D; :: thesis: for f being Function of D,NAT holds f * T is FinSequence of REAL
let f be Function of D,NAT ; :: thesis: f * T is FinSequence of REAL
( rng T c= D & dom f = D ) by FINSEQ_1:def 4, FUNCT_2:def 1;
then A1: f * T is FinSequence by FINSEQ_1:20;
rng (f * T) c= REAL ;
hence f * T is FinSequence of REAL by A1, FINSEQ_1:def 4; :: thesis: verum