s . a in pi (product SCMPDS-OK ),a by CARD_3:def 6;
then s . a in INT by Th24;
hence s . a is Integer ; :: thesis: verum