let G be non empty good 1-sorted ; :: thesis: for i being Element of SCM-Memory holds
( (SCM-OK G) . i = SCM-Instr G iff i in NAT )
let i be Element of SCM-Memory ; :: thesis: ( (SCM-OK G) . i = SCM-Instr G iff i in NAT )
thus ( (SCM-OK G) . i = SCM-Instr G implies i in NAT ) :: thesis: ( i in NAT implies (SCM-OK G) . i = SCM-Instr G )

proof

assume A1: (SCM-OK G) . i = SCM-Instr G ; :: thesis: i in NAT
assume A2: not i in NAT ; :: thesis: contradiction

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

suppose i = NAT ; :: thesis: contradiction

then (SCM-OK G) . i = NAT by Def3;
hence contradiction by A1, Th1; :: thesis: verum

end;

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

then (SCM-OK G) . i = the carrier of G by Def3;
hence contradiction by A1, Def2; :: thesis: verum

end;

end;

end;

thus ( i in NAT implies (SCM-OK G) . i = SCM-Instr G ) by Def3; :: thesis: verum