A1: Values lb = INT by SCMFSA_2:11;
b is Element of INT by INT_1:def 2;
then reconsider b = b as Element of Values lb by A1;
A2: Values la = INT by SCMFSA_2:11;
a is Element of INT by INT_1:def 2;
then reconsider a = a as Element of Values la by A2;
(la,lb) --> (a,b) is PartState of SCM+FSA ;
hence (la,lb) --> (a,b) is PartState of SCM+FSA ; :: thesis: verum