consider W being Tree;
consider d being Element of D;
set f = W --> d;
A1: dom (W --> d) = W by FUNCOP_1:19;
reconsider f = W --> d as DecoratedTree by A1, Def8;
A2: f is D -valued ;
thus ex b₁ being Function st
( b₁ is DecoratedTree-like & b₁ is D -valued ) by A2; :: thesis: verum