theorem Th4: :: SCMFSA_1:9

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