let G be non empty 1-sorted ; :: thesis: pi ((product ((SCM-VAL G) * SCM-OK)),NAT) = NAT
NAT in dom ((SCM-VAL G) * SCM-OK) by Lm1, AMI_2:22;
hence pi ((product ((SCM-VAL G) * SCM-OK)),NAT) = ((SCM-VAL G) * SCM-OK) . NAT by CARD_3:12
.= NAT by Th1 ;
:: thesis: verum