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