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