let X be non empty disjoint_with_NAT set ; :: thesis: for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 1 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
p = {}
set S = ECIW-signature ;
set G = DTConUA (ECIW-signature,X);
set A = FreeUnivAlgNSG (ECIW-signature,X);
let p be FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)); :: thesis: ( 1 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) implies p = {} )
assume 1 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) ; :: thesis: p = {}
then reconsider I = 1 -tree p as Element of (FreeUnivAlgNSG (ECIW-signature,X)) ;
per cases ( ex x being Element of X st I = root-tree x or ex n being Nat ex p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st
( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n ) ) by Th56;
suppose ex x being Element of X st I = root-tree x ; :: thesis: p = {}
then consider x being Element of X such that
A1: 1 -tree p = root-tree x ;
1 -tree p = x -tree (<*> (TS (DTConUA (ECIW-signature,X)))) by A1, TREES_4:20;
hence p = {} by TREES_4:15; :: thesis: verum
end;
suppose ex n being Nat ex p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st
( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n ) ; :: thesis: p = {}
then consider n being Nat, q being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) such that
n in Seg 4 and
A2: I = n -tree q and
A3: len q = ECIW-signature . n ;
q = p by A2, TREES_4:15;
hence p = {} by A2, A3, Th54, TREES_4:15; :: thesis: verum
end;
end;