pi ((product (SCM-VAL * SCM-OK)),NAT) = NAT by Th1, Lm5, Lm3, CARD_3:12;