( rng p c= D & D = dom h ) by FUNCT_2:def 1;
then A1: ( dom (h * p) = dom p & dom p = Seg (len p) ) by RELAT_1:27, FINSEQ_1:def 3;
then reconsider hp = h * p as FinSequence by FINSEQ_1:def 2;
len hp = len p by A1, FINSEQ_3:29;
hence ( h * p is len p -element & h * p is FinSequence-like ) by CARD_1:def 7; :: thesis: verum