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