let x be set ; :: thesis: for U being non empty set holds (U -multiCat) . x = (MultPlace (U -concatenation)) . x
let U be non empty set ; :: thesis: (U -multiCat) . x = (MultPlace (U -concatenation)) . x
set D = U * ;
set f = U -concatenation ;
set F = MultPlace (U -concatenation);
set G = U -multiCat ;
set g = {} .--> {};
reconsider g = {} .--> {} as {{}} -valued Function ;
( dom (U -concatenation) = [:(U *),(U *):] & dom (MultPlace (U -concatenation)) = ((U *) *) \ {{}} & dom (U -multiCat) = (U *) * ) by FUNCT_2:def 1;
then reconsider dF = dom (MultPlace (U -concatenation)) as Subset of (dom (U -multiCat)) ;

per cases ( x in dom (MultPlace (U -concatenation)) or not x in dom (MultPlace (U -concatenation)) ) ;

suppose x in dom (MultPlace (U -concatenation)) ; :: thesis: (U -multiCat) . x = (MultPlace (U -concatenation)) . x

hence (U -multiCat) . x = (MultPlace (U -concatenation)) . x by FUNCT_4:13; :: thesis: verum

end;

suppose A1: not x in dom (MultPlace (U -concatenation)) ; :: thesis: (U -multiCat) . x = (MultPlace (U -concatenation)) . x

hence (U -multiCat) . x = g . x by FUNCT_4:11
.= (MultPlace (U -concatenation)) . x by FUNCT_1:def 2, A1 ;
:: thesis: verum

end;

end;