per cases ( IC in dom p or not IC in dom p ) ;

suppose A1: IC in dom p ; :: thesis: p . (IC ) is Element of NAT

consider s being State of S such that
A2: p c= s by PBOOLE:141;
reconsider ss = s as Element of product (the_Values_of S) by CARD_3:107;
dom (the_Values_of S) = the carrier of S by PARTFUN1:def 2;
then pi ((product (the_Values_of S)),(IC )) = Values (IC ) by CARD_3:12
.= NAT by Def6 ;
then ss . (IC ) in NAT by CARD_3:def 6;
hence p . (IC ) is Element of NAT by A1, A2, GRFUNC_1:2; :: thesis: verum

end;

suppose not IC in dom p ; :: thesis: p . (IC ) is Element of NAT

then p . (IC ) = 0 by FUNCT_1:def 2;
hence p . (IC ) is Element of NAT ; :: thesis: verum

end;

end;