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

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

consider s being State of S such that
A2: p c= s by PBOOLE:156;
reconsider ss = s as Element of product the Object-Kind of S by PBOOLE:155;
dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then pi (product the Object-Kind of S),(IC S) = ObjectKind (IC S) by CARD_3:22
.= NAT by Def11 ;
then ss . (IC S) in NAT by CARD_3:def 6;
hence p . (IC S) is Element of NAT by A1, A2, GRFUNC_1:8; :: thesis: verum

end;

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

hence p . (IC S) is Element of NAT by FUNCT_1:def 4; :: thesis: verum

end;

end;