( a is Element of INT & ObjectKind la = INT ) by Th55, INT_1:def 2;
hence la .--> a is FinPartState of SCM by COMPOS_1:5; :: thesis: verum