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