A1: ObjectKind lb = INT by SCMFSA_2:26;
A2: ObjectKind la = INT by SCMFSA_2:26;
A3: b is Element of INT by INT_1:def 2;
a is Element of INT by INT_1:def 2;
hence la,lb --> a,b is FinPartState of SCM+FSA by A3, A2, A1, COMPOS_1:4; :: thesis: verum