dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;
then pi (product the Object-Kind of S),l = ObjectKind l by CARD_3:22
.= the Instructions of S by Def14 ;
hence s . l is Instruction of S by CARD_3:def 6; :: thesis: verum