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, AMI_1:59; :: thesis: verum