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 & I = o -tree p ) by Th16;
A3: 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 A4: o in NonTerminals (DTConUA ECIW-signature ,X) by A2;
A5: NonTerminals (DTConUA ECIW-signature ,X) = Seg 4 by Th54, FREEALG:2;
then reconsider n = o as Element of NAT by A4;
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, A3, A5; :: thesis: ( I = n -tree p & len p = ECIW-signature . n )
thus I = n -tree p by A2; :: thesis: len p = ECIW-signature . n
A6: [n,(roots p)] in the Rules of (DTConUA ECIW-signature ,X) by A2, LANG1:def 1;
then A7: 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 PRE_CIRC:21
.= len (roots p) by PRE_CIRC:21
.= ECIW-signature . n by A6, A7, FREEALG:def 8 ;
:: thesis: verum