let D be non empty set ; :: thesis: {} .--> {} tolerates MultPlace (D -concatenation)
set f = {} .--> {};
set g = MultPlace (D -concatenation);
( dom ({} .--> {}) = {{}} & dom (MultPlace (D -concatenation)) = ((D *) *) \ {{}} ) by FUNCT_2:def 1;
then for x being object st x in (dom (MultPlace (D -concatenation))) /\ (dom ({} .--> {})) holds
({} .--> {}) . x = (MultPlace (D -concatenation)) . x by XBOOLE_1:79, XBOOLE_0:def 7;
hence {} .--> {} tolerates MultPlace (D -concatenation) by PARTFUN1:def 4; :: thesis: verum