Y: dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
U: l in NAT ;
NAT c= the carrier of S by Def3;
then X: pi (product the Object-Kind of S),l = the Object-Kind of S . l by Y, U, CARD_3:22
.= the Instructions of S by Def14 ;
s in product the Object-Kind of S by PBOOLE:155;
hence s . l is Instruction of S by X, CARD_3:def 6; :: thesis: verum