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