thus dom (P --> 0 ) = P by FUNCOP_1:19; :: according to PNPROC_1:def 1 :: thesis: rng (P --> 0 ) c= NAT
rng (P --> 0 ) c= {0 } by FUNCOP_1:19;
hence rng (P --> 0 ) c= NAT by XBOOLE_1:1; :: thesis: verum