dom (SCM*-VAL * SCM+FSA-OK) = SCM+FSA-Memory by Lm8;
then A1: pi ((product (SCM*-VAL * SCM+FSA-OK)),a) = (SCM*-VAL * SCM+FSA-OK) . a by CARD_3:12
.= INT by Th5 ;
s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def 6;
hence s . a is integer by A1; :: thesis: verum