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