( {} in (D *) * & {} in D * )
by FINSEQ_1:66;
then Z1:
( {{}} c= (D *) * & {{}} c= D * )
by ZFMISC_1:37;
then A0:
( {{}} \/ ((D *) *) = (D *) * & {{}} \/ (D *) = D * )
by XBOOLE_1:12;
set f = {} .--> {};
set g = MultPlace (D -concatenation);
A1:
( dom ({} .--> {}) = {{}} & rng ({} .--> {}) c= {{}} )
by FUNCOP_1:19;
A2:
( 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, A1, A2;
then A4:
(dom ({} .--> {})) \/ (dom (MultPlace (D -concatenation))) = (D *) *
by Z1, XBOOLE_1:12;
( (rng ({} .--> {})) \/ (rng (MultPlace (D -concatenation))) c= D * & rng (({} .--> {}) +* (MultPlace (D -concatenation))) c= (rng ({} .--> {})) \/ (rng (MultPlace (D -concatenation))) )
by A0, A1, XBOOLE_1:13, FUNCT_4:18;
then
( dom (D -multiCat) = (D *) * & rng (D -multiCat) c= D * )
by FUNCT_4:def 1, A4, XBOOLE_1:1;
hence
D -multiCat is Function of ((D *) *),(D *)
by RELSET_1:11, FUNCT_2:130; verum