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