la,lb --> a,b = (la .--> a) +* (lb .--> b) by FUNCT_4:def 4;
hence la,lb --> a,b is FinPartState of SCMPDS ; :: thesis: verum