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