let D be non empty set ; :: thesis: for d being non empty Element of (D *) * holds (D -multiCat) . d = (MultPlace (D -concatenation)) . d
let d be non empty Element of (D *) * ; :: thesis: (D -multiCat) . d = (MultPlace (D -concatenation)) . d
set f = D -concatenation ;
set F = D -multiCat ;
not d in {{}} by TARSKI:def 1;
then d in ((D *) *) \ {{}} by XBOOLE_0:def 5;
hence (D -multiCat) . d = ((D -multiCat) | (((D *) *) \ {{}})) . d by FUNCT_1:49
.= (MultPlace (D -concatenation)) . d by Lm23 ;
:: thesis: verum