let X be non empty disjoint_with_NAT set ; :: thesis: for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X))
for x being Element of X st x -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
p = {}
set S = ECIW-signature ;
set A = FreeUnivAlgNSG (ECIW-signature,X);
let p be FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)); :: thesis: for x being Element of X st x -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
p = {}
let x be Element of X; :: thesis: ( x -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) implies p = {} )
assume x -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) ; :: thesis: p = {}
then reconsider I = x -tree p as Element of (FreeUnivAlgNSG (ECIW-signature,X)) ;
now :: thesis: for n being Nat
for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) holds
( not n in Seg 4 or not I = n -tree p or not len p = ECIW-signature . n )
given n being Nat, p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) 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