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
.= IL by Def11 ;
then s . (IC S) in IL by CARD_3:def 6;
hence s . (IC S) is Instruction-Location of S by Def4; :: thesis: verum