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