( a is Element of INT & ObjectKind la = INT ) by INT_1:def 2, SCMFSA_2:11;
hence la .--> a is FinPartState of SCM+FSA ; :: thesis: verum