A1: rng P = dom f by FUNCT_2:def 3;
then dom (P * f) = dom P by RELAT_1:27;
then dom (P * f) = dom f by FUNCT_2:52;
then ex n being Nat st dom (P * f) = Seg n by FINSEQ_1:def 2;
then reconsider F = P * f as FinSequence by FINSEQ_1:def 2;
rng F = rng f by A1, RELAT_1:28;
hence P * f is FinSequence of D by FINSEQ_1:def 4; :: thesis: verum