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