dom SCM+FSA-OK = SCM+FSA-Memory by FUNCT_2:def 1;
then A1: pi ((product SCM+FSA-OK),a) = SCM+FSA-OK . a by CARD_3:12
.= INT by Th10 ;
s . a in pi ((product SCM+FSA-OK),a) by CARD_3:def 6;
hence s . a is Integer by A1; :: thesis: verum