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:22
.= INT * by Th12 ;
s . a in pi (product SCM+FSA-OK ),a by CARD_3:def 6;
hence s . a is FinSequence of INT by A1, FINSEQ_1:def 11; :: thesis: verum