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