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:106;
dom p = dom (roots p) by TREES_3:def 18;
hence len p = card (dom (roots p)) by CARD_1:104
.= len (roots p) by CARD_1:104
.= ECIW-signature . n by A7, A8, FREEALG:def 8 ;
:: thesis: verum