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