set IT = p +~ (x,y);
dom (p +~ (x,y)) = dom p by FUNCT_4:99
.= Seg (len p) by FINSEQ_1:def 3 ;
hence p +~ (x,y) is FinSequence-like ; :: thesis: verum