let D be non empty set ; :: thesis: (D -multiCat) | (((D *) *) \ {{}}) = MultPlace (D -concatenation)
set f = D -concatenation ;
set F = MultPlace (D -concatenation);
dom (MultPlace (D -concatenation)) = ((D *) *) \ {{}} by FUNCT_2:def 1;
hence (D -multiCat) | (((D *) *) \ {{}}) = MultPlace (D -concatenation) ; :: thesis: verum