let Y be set ; :: thesis: for D being non empty set holds (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y
let D be non empty set ; :: thesis: (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y
set F = D -multiCat ;
(D -multiCat) | (Y \ {{}}) = ((D -multiCat) | ((D *) *)) | (Y \ {{}})
.= (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 Lm23 ;
hence (D -multiCat) | (Y \ {{}}) = (MultPlace (D -concatenation)) | Y ; :: thesis: verum