( t is Element of INT * & ObjectKind f = INT * ) by FINSEQ_1:def 11, SCMFSA_2:27;
hence f .--> t is FinPartState of SCM+FSA by AMI_1:59; :: thesis: verum