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