A1: ( {{}} c= (D *) * & {{}} c= D * ) by ZFMISC_1:31, FINSEQ_1:49;
then A2: ( {{}} \/ ((D *) *) = (D *) * & {{}} \/ (D *) = D * ) by XBOOLE_1:12;
set f = {} .--> {};
set g = MultPlace (D -concatenation);
A3: ( dom ({} .--> {}) = {{}} & rng ({} .--> {}) c= {{}} ) by FUNCOP_1:13;
A4: ( dom (MultPlace (D -concatenation)) = ((D *) *) \ {{}} & rng (MultPlace (D -concatenation)) c= D * ) by FUNCT_2:def 1;
(dom ({} .--> {})) \/ (dom (MultPlace (D -concatenation))) = {{}} \/ ((D *) *) by XBOOLE_1:39, A4;
then A5: (dom ({} .--> {})) \/ (dom (MultPlace (D -concatenation))) = (D *) * by A1, XBOOLE_1:12;
( (rng ({} .--> {})) \/ (rng (MultPlace (D -concatenation))) c= D * & rng (({} .--> {}) +* (MultPlace (D -concatenation))) c= (rng ({} .--> {})) \/ (rng (MultPlace (D -concatenation))) ) by A2, A3, XBOOLE_1:13, FUNCT_4:17;
then ( dom (D -multiCat) = (D *) * & rng (D -multiCat) c= D * ) by FUNCT_4:def 1, A5;
hence D -multiCat is Function of ((D *) *),(D *) by RELSET_1:4, FUNCT_2:67; :: thesis: verum