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