theorem :: SCMRING2:24

for R being Ring holds the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;