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