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 NAT
let T be FinSequence of D; :: thesis: for f being Function of D,NAT holds f * T is FinSequence of NAT
let f be Function of D,NAT ; :: thesis: f * T is FinSequence of NAT
A1: rng T c= D by FINSEQ_1:def 4;
dom f = D by FUNCT_2:def 1;
then A2: f * T is FinSequence by A1, FINSEQ_1:20;
rng (f * T) c= NAT by RELAT_1:def 19;
hence f * T is FinSequence of NAT by A2, FINSEQ_1:def 4; :: thesis: verum