per cases
( x in the ColoredSet of CPN or not x in the ColoredSet of CPN )
;

end;

suppose
not x in the ColoredSet of CPN
; :: thesis: mp . x is Element of NAT

then
not x in dom mp
;

then mp . x = 0 by FUNCT_1:def 2;

hence mp . x is Element of NAT ; :: thesis: verum

end;then mp . x = 0 by FUNCT_1:def 2;

hence mp . x is Element of NAT ; :: thesis: verum