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