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

then consider x being Element of X such that
A1: 3 -tree p = root-tree x ;
3 -tree p = x -tree (<*> (TS (DTConUA (ECIW-signature,X)))) by A1, TREES_4:20;
then 3 = x by TREES_4:15;
then X meets NAT by XBOOLE_0:3;
hence ex C, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,I1,I2*> 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, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,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 = 3 by A2, TREES_4:15;
A5: q = p by A2, TREES_4:15;
then p = <*(p . 1),(p . 2),(p . 3)*> by A3, A4, Th54, FINSEQ_1:45;
then A6: rng p = {(p . 1),(p . 2),(p . 3)} by FINSEQ_2:128;
A7: p . 1 in {(p . 1),(p . 2),(p . 3)} by ENUMSET1:def 1;
A8: p . 2 in {(p . 1),(p . 2),(p . 3)} by ENUMSET1:def 1;
p . 3 in {(p . 1),(p . 2),(p . 3)} by ENUMSET1:def 1;
then reconsider C = p . 1, I1 = p . 2, I2 = p . 3 as Element of (FreeUnivAlgNSG (ECIW-signature,X)) by A6, A7, A8;
take C ; :: thesis: ex I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,I1,I2*>
take I1 ; :: thesis: ex I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,I1,I2*>
take I2 ; :: thesis: p = <*C,I1,I2*>
thus p = <*C,I1,I2*> by A3, A4, A5, Th54, FINSEQ_1:45; :: thesis: verum

end;

end;