let ts be FinSequence of T; :: thesis: ts is DTree-yielding
thus ts is DTree-yielding ; :: thesis: verum