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 CARD_3:22, Y, U
.= 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 CARD_3:def 6, X; :: thesis: verum