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