let I be Instruction of SCMPDS ; :: thesis: ( I in { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } implies InsCode I = 1 )
assume I in { [1,{} ,<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; :: thesis: InsCode I = 1
then ex d1 being Element of SCM-Data-Loc st I = [1,{} ,<*d1*>] ;
hence InsCode I = 1 by RECDEF_2:def 1; :: thesis: verum