A1: dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
A2: l in NAT ;
NAT c= the carrier of S by Def2;
then A3: pi ((product the Object-Kind of S),l) = the Object-Kind of S . l by A1, A2, CARD_3:22
.= the Instructions of S by Def8 ;
s in product the Object-Kind of S by PBOOLE:155;
hence s . l is Instruction of S by A3, CARD_3:def 6; :: thesis: verum