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