let D be non empty set ; :: thesis: for Y being set holds (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y
let Y be set ; :: thesis: (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y
set F = D -multiCat ;
B1: dom (D -multiCat) = (D *) * by FUNCT_2:def 1;
(D -multiCat) | (Y \ {{}}) = ((D -multiCat) | ((D *) *)) | (Y \ {{}}) by B1, RELAT_1:69
.= (D -multiCat) | (((D *) *) /\ (Y \ {{}})) by RELAT_1:71
.= (D -multiCat) | ((((D *) *) /\ Y) \ {{}}) by XBOOLE_1:49
.= (D -multiCat) | (Y /\ (((D *) *) \ {{}})) by XBOOLE_1:49
.= ((D -multiCat) | (((D *) *) \ {{}})) | Y by RELAT_1:71
.= (MultPlace (D -concatenation)) | Y by Lm6 ;
hence (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y ; :: thesis: verum