let I be Instruction of SCMPDS ; :: thesis: ( I in { [0 ,<*k1*>] where k1 is Element of INT : verum } implies InsCode I = 0 )
assume I in { [0 ,<*k1*>] where k1 is Element of INT : verum } ; :: thesis: InsCode I = 0
then consider k1 being Element of INT such that
A1: I = [0 ,<*k1*>] ;
thus InsCode I = 0 by A1, MCART_1:7; :: thesis: verum