theorem Th1: :: AMI_2:6

(SCM-VAL * SCM-OK) . NAT = NAT