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 Th6 ;

s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def 6;

hence s . a is FinSequence of INT by A1, FINSEQ_1:def 11; :: thesis: verum

then A1: pi ((product (SCM*-VAL * SCM+FSA-OK)),a) = (SCM*-VAL * SCM+FSA-OK) . a by CARD_3:12

.= INT * by Th6 ;

s . a in pi ((product (SCM*-VAL * SCM+FSA-OK)),a) by CARD_3:def 6;

hence s . a is FinSequence of INT by A1, FINSEQ_1:def 11; :: thesis: verum