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 ex k1 being Element of INT st I = [0 ,<*k1*>] ;
hence InsCode I = 0 by MCART_1:7; :: thesis: verum