A1: t is Element of INT * by FINSEQ_1:def 11;
Values f = INT * by SCMFSA_2:12;
hence f .--> t is the_Values_of SCM+FSA -compatible by A1; :: thesis: verum