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 consider d1 being Element of SCM-Data-Loc such that
A1: I = [1,<*d1*>] ;
thus InsCode I = 1 by A1, MCART_1:7; :: thesis: verum