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