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

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

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

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;

end;