let D be non empty set ; :: thesis: for T being DecoratedTree of D holds T is Function of dom T,D
let T be DecoratedTree of D; :: thesis: T is Function of dom T,D
rng T c= D by TREES_2:def 9;
hence T is Function of dom T,D by FUNCT_2:def 1, RELSET_1:11; :: thesis: verum