let i1 be Element of NAT ; :: thesis: for G being non empty good 1-sorted holds (SCM-OK G) . i1 = SCM-Instr G
let G be non empty good 1-sorted ; :: thesis: (SCM-OK G) . i1 = SCM-Instr G
i1 in NAT ;
then reconsider i1 = i1 as Element of SCM-Memory by Lm2;
(SCM-OK G) . i1 = SCM-Instr G by Th4;
hence (SCM-OK G) . i1 = SCM-Instr G ; :: thesis: verum