let X be non empty disjoint_with_NAT set ; 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)); ( 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
; 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
; 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
; ( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n )
thus
n in Seg 4
by A2, A4, A6; ( I = n -tree p & len p = ECIW-signature . n )
thus
I = n -tree p
by A3; 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
;
verum