reconsider b9 = b as Element of ObjectKind lb by Th1;
reconsider a9 = a as Element of ObjectKind la by Th1;
(la,lb) --> (a9,b9) is FinPartState of (SCM R) ;
hence (la,lb) --> (a,b) is FinPartState of (SCM R) ; :: thesis: verum