set g = MultPlace (D -concatenation);
set f = {} .--> {};
( dom ({} .--> {}) = {{}} & dom (MultPlace (D -concatenation)) = ((D *) *) \ {{}} ) by FUNCT_2:def 1;
then {} in dom ({} .--> {}) by TARSKI:def 1;
then A1: ( {} in dom ({} .--> {}) & {} in (dom (MultPlace (D -concatenation))) \/ (dom ({} .--> {})) ) by XBOOLE_0:def 3;
{} .--> {} tolerates MultPlace (D -concatenation) by Lm9;
then D -multiCat = (MultPlace (D -concatenation)) +* ({} .--> {}) by FUNCT_4:34;
then ( e = {} & (D -multiCat) . {} = ({} .--> {}) . {} ) by A1, FUNCT_4:def 1;
hence for b₁ being set st b₁ = (D -multiCat) . e holds
b₁ is empty by FUNCOP_1:72; :: thesis: verum