dom (p +* i,x) = dom p by FUNCT_7:32;
hence ( p +* i,x is finite & p +* i,x is T-Sequence-like ) by FINSET_1:29, ORDINAL1:def 7; :: thesis: verum