dom (W --> x) = W by FUNCOP_1:13;
hence W --> x is DecoratedTree-like by Def8; :: thesis: verum