let f be Function; :: thesis: ( f is DTree-yielding implies f is Function-yielding )
assume A1: rng f is constituted-DTrees ; :: according to TREES_3:def 11 :: thesis: f is Function-yielding
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
then f . x in rng f by FUNCT_1:3;
then f . x is DecoratedTree by A1;
hence f . x is Function ; :: thesis: verum