let X be non empty disjoint_with_NAT set ; :: thesis: for I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
( 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 ) )
set S = ECIW-signature ;
set G = DTConUA (ECIW-signature,X);
let I be Element of (FreeUnivAlgNSG (ECIW-signature,X)); :: thesis: ( 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 ) )
assume A1: for x being Element of X holds not I = root-tree x ; :: thesis: 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 )
Terminals (DTConUA (ECIW-signature,X)) = X by FREEALG:3;
then for d being Symbol of (DTConUA (ECIW-signature,X)) holds
( not d in Terminals (DTConUA (ECIW-signature,X)) or not I = root-tree d ) by A1;
then consider o being Symbol of (DTConUA (ECIW-signature,X)), p being FinSequence of TS (DTConUA (ECIW-signature,X)) such that
A2: o ==> roots p and
A3: I = o -tree p by Th16;
A4: NonTerminals (DTConUA (ECIW-signature,X)) = { s where s is Symbol of (DTConUA (ECIW-signature,X)) : ex n being FinSequence st s ==> n } by LANG1:def 3;
then A5: o in NonTerminals (DTConUA (ECIW-signature,X)) by A2;
A6: NonTerminals (DTConUA (ECIW-signature,X)) = Seg 4 by Th54, FREEALG:2;
then reconsider n = o as Element of NAT by A5;
reconsider p = p as FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) ;
take n ; :: thesis: ex p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st
( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n )
take p ; :: thesis: ( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n )
thus n in Seg 4 by A2, A4, A6; :: thesis: ( I = n -tree p & len p = ECIW-signature . n )
thus I = n -tree p by A3; :: thesis: len p = ECIW-signature . n
A7: [n,(roots p)] in the Rules of (DTConUA (ECIW-signature,X)) by A2, LANG1:def 1;
then A8: roots p in the carrier of (DTConUA (ECIW-signature,X)) * by ZFMISC_1:87;
dom p = dom (roots p) by TREES_3:def 18;
hence len p = card (dom (roots p)) by CARD_1:62
.= len (roots p) by CARD_1:62
.= ECIW-signature . n by A7, A8, FREEALG:def 7 ;
:: thesis: verum