A1: dom F = NAT by FUNCT_2:def 1;
A2: dom (F +* p) = (dom F) \/ (dom p) by FUNCT_4:def 1
.= NAT by A1, XBOOLE_1:12 ;
A3: rng (F +* p) c= (rng F) \/ (rng p) by FUNCT_4:18;
A4: rng F c= A by RELAT_1:def 19;
rng p c= A by FINSEQ_1:def 4;
then (rng F) \/ (rng p) c= A by A4, XBOOLE_1:8;
then rng (F +* p) c= A by A3, XBOOLE_1:1;
hence F +* p is Function of NAT ,A by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum