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 RECDEF_2:def 1; :: thesis: verum