let i1 be Element of NAT ; :: thesis: pi ((product SCMPDS-OK),i1) = SCMPDS-Instr
i1 in NAT ;
then reconsider n = i1 as Element of SCM-Memory by Lm2;
dom SCMPDS-OK = SCM-Memory by FUNCT_2:def 1;
hence pi ((product SCMPDS-OK),i1) = SCMPDS-OK . n by CARD_3:22
.= SCMPDS-Instr by Th20 ;
:: thesis: verum