let i1 be Element of NAT ; :: thesis: SCMPDS-OK . i1 = SCMPDS-Instr
i1 in NAT ;
then reconsider i1 = i1 as Element of SCM-Memory by Lm2;
SCMPDS-OK . i1 = SCMPDS-Instr by Th20;
hence SCMPDS-OK . i1 = SCMPDS-Instr ; :: thesis: verum