reconsider G = F as Function ;
A1: h " (dom G) = h " (rng h) by FUNCT_2:def 3
.= dom h by RELAT_1:134 ;
dom (G * h) = h " (dom G) by RELAT_1:147
.= dom F by A1, FUNCT_2:52
.= Seg (len F) by FINSEQ_1:def 3 ;
then A2: F * h is FinSequence by FINSEQ_1:def 2;
rng (F * h) c= D ;
hence F * h is FinSequence of D by A2, FINSEQ_1:def 4; :: thesis: verum