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

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