ex X being non empty set st the Instructions of S c= [:NAT ,(NAT * ),(X * ):] by Def32;
then dom the Instructions of S c= [:NAT ,(NAT * ):] by FUNCT_5:13;
then reconsider II = dom the Instructions of S as Relation ;
assume InsCodes S is empty ; :: thesis: contradiction
then II = {} ;
hence contradiction ; :: thesis: verum