A1: ( ObjectKind la = INT & ObjectKind lb = INT ) by SCMPDS_2:13;
( a is Element of INT & b is Element of INT ) by INT_1:def 2;
hence (la,lb) --> (a,b) is FinPartState of SCMPDS by A1, COMPOS_1:4; :: thesis: verum