A1: dom (W --> x) = W by FUNCOP_1:19;
thus W --> x is DecoratedTree-like by A1, Def8; :: thesis: verum