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
( 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 c= NAT & rng (f * T) c= rng f ) by RELAT_1:45, RELAT_1:def 19;
then rng (f * T) c= NAT by XBOOLE_1:1;
hence f * T is FinSequence of NAT by A1, FINSEQ_1:def 4; :: thesis: verum