s . a in pi ((product ((SCM-VAL R) * SCM-OK)),a) by CARD_3:def 6;
hence s . a is Element of R by Th5; :: thesis: verum