let p be FinSequence of (Free S,X); :: thesis: p is DTree-yielding
let x be set ; :: according to TREES_3:def 5,TREES_3:def 11 :: thesis: ( not x in rng p or x is set )
assume x in rng p ; :: thesis: x is set
then x is Element of (Free S,X) ;
hence x is set ; :: thesis: verum