A1: rng P = dom f by FUNCT_2:def 3;
then dom (P * f) = dom P by RELAT_1:46;
then dom (P * f) = dom f by FUNCT_2:67;
then consider n being Nat such that
A2: dom (P * f) = Seg n by FINSEQ_1:def 2;
reconsider F = P * f as FinSequence by A2, FINSEQ_1:def 2;
rng F = rng f by A1, RELAT_1:47;
hence P * f is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum