A1:
( Values la = INT & Values lb = INT )
by SCMPDS_2:5;

A2: ( a is Element of INT & b is Element of INT ) by INT_1:def 2;

reconsider a = a as Element of Values la by A1, A2;

reconsider b = b as Element of Values lb by A1, A2;

(la,lb) --> (a,b) is PartState of SCMPDS ;

hence (la,lb) --> (a,b) is PartState of SCMPDS ; :: thesis: verum

A2: ( a is Element of INT & b is Element of INT ) by INT_1:def 2;

reconsider a = a as Element of Values la by A1, A2;

reconsider b = b as Element of Values lb by A1, A2;

(la,lb) --> (a,b) is PartState of SCMPDS ;

hence (la,lb) --> (a,b) is PartState of SCMPDS ; :: thesis: verum