theorem Th4: :: SCMRING1:5

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