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