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