theorem Th4: :: AMI_2:9

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