let f be Function; :: thesis: ( f is DTree-yielding iff for x being object st x in dom f holds
f . x is DecoratedTree )
thus ( f is DTree-yielding implies for x being object st x in dom f holds
f . x is DecoratedTree ) :: thesis: ( ( for x being object st x in dom f holds
f . x is DecoratedTree ) implies f is DTree-yielding )

proof

assume A1: for x being object st x in rng f holds
x is DecoratedTree ; :: according to TREES_3:def 5,TREES_3:def 11 :: thesis: for x being object st x in dom f holds
f . x is DecoratedTree
let x be object ; :: thesis: ( x in dom f implies f . x is DecoratedTree )
assume x in dom f ; :: thesis: f . x is DecoratedTree
then f . x in rng f by FUNCT_1:def 3;
hence f . x is DecoratedTree by A1; :: thesis: verum

end;

assume A2: for x being object st x in dom f holds
f . x is DecoratedTree ; :: thesis: f is DTree-yielding
let x be object ; :: according to TREES_3:def 5,TREES_3:def 11 :: thesis: ( x in rng f implies x is DecoratedTree )
assume x in rng f ; :: thesis: x is DecoratedTree
then ex y being object st
( y in dom f & x = f . y ) by FUNCT_1:def 3;
hence x is DecoratedTree by A2; :: thesis: verum