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 ;
hence T is Function of (dom T),D by FUNCT_2:def 1, RELSET_1:4; :: thesis: verum