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 Object-Kind of S by CARD_3:107;
dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then pi ((product the Object-Kind of S),(IC )) = ObjectKind (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;