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