let i1 be Element of NAT ; :: thesis: for G being non empty good 1-sorted holds pi (product (SCM-OK G)),i1 = SCM-Instr G
let G be non empty good 1-sorted ; :: thesis: pi (product (SCM-OK G)),i1 = SCM-Instr G
dom (SCM-OK G) = SCM-Memory by FUNCT_2:def 1;
hence pi (product (SCM-OK G)),i1 = (SCM-OK G) . i1 by CARD_3:22
.= SCM-Instr G by Th4 ;
:: thesis: verum