let X be non empty disjoint_with_NAT set ; :: thesis: for p being FinSequence of
for x being Element of X st x -tree p is Element of holds
p = {}
set S = ECIW-signature ;
set A = FreeUnivAlgNSG ECIW-signature ,X;
let p be FinSequence of ; :: thesis: for x being Element of X st x -tree p is Element of holds
p = {}
let x be Element of X; :: thesis: ( x -tree p is Element of implies p = {} )
assume x -tree p is Element of ; :: thesis: p = {}
then reconsider I = x -tree p as Element of ;

now

given n being Nat, p being FinSequence of such that A1: n in Seg 4 and
A2: I = n -tree p and
len p = ECIW-signature . n ; :: thesis: contradiction
A3: x = n by A2, TREES_4:15;
X misses NAT by FREEALG:def 1;
hence contradiction by A1, A3, XBOOLE_0:3; :: thesis: verum

end;

then consider y being Element of X such that
A4: I = root-tree y by Th56;
x -tree p = y -tree {} by A4, TREES_4:20;
hence p = {} by TREES_4:15; :: thesis: verum