let i be Element of SCM-Memory ; :: thesis: ( SCMPDS-OK . i = SCMPDS-Instr iff i in NAT )
thus ( SCMPDS-OK . i = SCMPDS-Instr implies i in NAT ) :: thesis: ( i in NAT implies SCMPDS-OK . i = SCMPDS-Instr )

proof

assume A1: SCMPDS-OK . i = SCMPDS-Instr ; :: thesis: i in NAT
assume A2: not i in NAT ; :: thesis: contradiction

per cases ( i = NAT or i in SCM-Data-Loc ) by A2, Th14;

suppose i = NAT ; :: thesis: contradiction

hence contradiction by A1, Def4, Th17; :: thesis: verum

end;

suppose i in SCM-Data-Loc ; :: thesis: contradiction

hence contradiction by A1, Def4, Th17; :: thesis: verum

end;

end;

end;

thus ( i in NAT implies SCMPDS-OK . i = SCMPDS-Instr ) by Def4; :: thesis: verum