A1: dom F = NAT by FUNCT_2:def 1;
dom (F +* p) = (dom F) \/ (dom p) by FUNCT_4:def 1
.= NAT by A1, XBOOLE_1:12 ;
hence F +* p is sequence of A by FUNCT_2:def 1; :: thesis: verum