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