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