set g = MultPlace (D -concatenation);
set f = {} .--> {};
{} in dom ({} .--> {}) by TARSKI:def 1;
then A1: ( {} in dom ({} .--> {}) & {} in (dom (MultPlace (D -concatenation))) \/ (dom ({} .--> {})) ) by XBOOLE_0:def 3;
D -multiCat = (MultPlace (D -concatenation)) +* ({} .--> {}) by Lm25, 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 ; :: thesis: verum