set W = the Tree;
set d = the Element of D;
set f = the Tree --> the Element of D;
dom ( the Tree --> the Element of D) = the Tree ;
then reconsider f = the Tree --> the Element of 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