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;
p is FinSequence of (Free (C,(MSVars C))) by A1, ThA1;
hence ex b₁ being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b₁ by A1, A2; :: thesis: verum