consider v being set , p being DTree-yielding FinSequence such that
A1: e = v -tree p by TREES_9:8;
A2: v = e . {} by A1, TREES_4:def 4;
thus ex b₁ being DTree-yielding FinSequence st e = (e . {}) -tree b₁ by A1, A2; :: thesis: verum