let X be non empty disjoint_with_NAT set ; for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 2 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds
ex I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*I1,I2*>
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)); ( 2 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) implies ex I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*I1,I2*> )
assume
2 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X))
; ex I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*I1,I2*>
then reconsider I = 2 -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
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 )
;
ex I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*I1,I2*>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
;
A4:
n = 2
by A2, TREES_4:15;
A5:
q = p
by A2, TREES_4:15;
then
p = <*(p . 1),(p . 2)*>
by A3, A4, Th54, FINSEQ_1:44;
then
rng p = {(p . 1),(p . 2)}
by FINSEQ_2:127;
then reconsider I1 =
p . 1,
I2 =
p . 2 as
Element of
(FreeUnivAlgNSG (ECIW-signature,X)) by ZFMISC_1:32;
take
I1
;
ex I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*I1,I2*>take
I2
;
p = <*I1,I2*>thus
p = <*I1,I2*>
by A3, A4, A5, Th54, FINSEQ_1:44;
verum end; end;