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