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