let X be non empty disjoint_with_NAT set ; :: thesis: for p being FinSequence of (FreeUnivAlgNSG ECIW-signature ,X) st 4 -tree p is Element of (FreeUnivAlgNSG ECIW-signature ,X) holds
ex C, I being Element of (FreeUnivAlgNSG ECIW-signature ,X) st p = <*C,I*>
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); :: thesis: ( 4 -tree p is Element of (FreeUnivAlgNSG ECIW-signature ,X) implies ex C, I being Element of (FreeUnivAlgNSG ECIW-signature ,X) st p = <*C,I*> )
assume 4 -tree p is Element of (FreeUnivAlgNSG ECIW-signature ,X) ; :: thesis: ex C, I being Element of (FreeUnivAlgNSG ECIW-signature ,X) st p = <*C,I*>
then reconsider I = 4 -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 x being Element of X st I = root-tree x ; :: thesis: ex C, I being Element of (FreeUnivAlgNSG ECIW-signature ,X) st p = <*C,I*>

then consider x being Element of X such that
A1: 4 -tree p = root-tree x ;
4 -tree p = x -tree (<*> (TS (DTConUA ECIW-signature ,X))) by A1, TREES_4:20;
then 4 = x by TREES_4:15;
then X meets NAT by XBOOLE_0:3;
hence ex C, I being Element of (FreeUnivAlgNSG ECIW-signature ,X) st p = <*C,I*> by FREEALG:def 1; :: thesis: verum

end;

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 ) ; :: thesis: ex C, I being Element of (FreeUnivAlgNSG ECIW-signature ,X) st p = <*C,I*>

then consider n being Nat, q being FinSequence of (FreeUnivAlgNSG ECIW-signature ,X) such that
A2: ( n in Seg 4 & I = n -tree q & len q = ECIW-signature . n ) ;
A3: ( n = 4 & q = p ) by A2, TREES_4:15;
then p = <*(p . 1),(p . 2)*> by A2, Th54, FINSEQ_1:61;
then rng p = {(p . 1),(p . 2)} by FINSEQ_2:147;
then reconsider I1 = p . 1, I2 = p . 2 as Element of (FreeUnivAlgNSG ECIW-signature ,X) by ZFMISC_1:38;
take I1 ; :: thesis: ex I being Element of (FreeUnivAlgNSG ECIW-signature ,X) st p = <*I1,I*>
take I2 ; :: thesis: p = <*I1,I2*>
thus p = <*I1,I2*> by A3, A2, Th54, FINSEQ_1:61; :: thesis: verum

end;

end;