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