let i, j be Nat; :: thesis: NPP ((intloc i) .--> j) = (intloc i) .--> j
not intloc i in NAT by SCMFSA10:3;
then A: intloc i in the carrier of SCM+FSA \ NAT by XBOOLE_0:def 5;
thus NPP ((intloc i) .--> j) = ((intloc i) .--> j) | ( the carrier of SCM+FSA \ NAT) by COMPOS_1:65
.= (intloc i) .--> j by A, FUNCOP_1:101 ; :: thesis: verum