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
.= the Instructions of S by Def14 ;
hence s . (IC s) is Instruction of S by CARD_3:def 6; :: thesis: verum