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