let p be FinSequence of D; :: thesis: p is DTree-yielding
let x be object ; :: according to TREES_3:def 5,TREES_3:def 11 :: thesis: ( x in rng p implies x is DecoratedTree )
rng p c= D ;
hence ( x in rng p implies x is DecoratedTree ) ; :: thesis: verum