( rng p c= D & dom h = D ) by PARTFUN1:def 2;
then dom (h * p) = dom p by RELAT_1:27;
then ex k being Nat st dom (h * p) = Seg k by FINSEQ_1:def 2;
hence h * p is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum