theorem Th1: :: SCMRING1:2

for G being non empty 1-sorted holds ((SCM-VAL G) * SCM-OK) . NAT = NAT