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