defpred S₁[ Nat] means ex T being DecoratedTree of F₁() st
( T . {} = F₂() & ( for t being Element of dom T holds
( len t <= $1 & ( len t < $1 implies ( succ t = { (t ^ <*k*>) where k is Nat : P₁[k,T . t] } & ( for n being Nat
for x being set st x = T . t & P₁[n,x] holds
T . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) );
reconsider W = {{}} as Tree ;
A2: S₁[ 0 ]

take T1 = W --> F₂(); :: thesis:
{} in W by TREES_1:22;
hence T1 . {} = F₂() by FUNCOP_1:7; :: thesis:
let t be Element of dom T1; :: thesis:
t = {} by TARSKI:def 1;
hence len t <= 0 ; :: thesis:
assume len t < 0 ; :: thesis:
hence ( succ t = { (t ^ <*k*>) where k is Nat : P₁[k,T1 . t] } & ( for n being Nat
for x being set st x = T1 . t & P₁[n,x] holds
T1 . (t ^ <*n*>) = F₃() . (x,n) ) ) ; :: thesis:

end;

A3: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
given T being DecoratedTree of F₁() such that A4: ( T . {} = F₂() & ( for t being Element of dom T holds
( len t <= k & ( len t < k implies ( succ t = { (t ^ <*m*>) where m is Nat : P₁[m,T . t] } & ( for n being Nat
for x being set st x = T . t & P₁[n,x] holds
T . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) ; :: thesis:
reconsider M = { (t ^ <*n*>) where n is Nat, t is Element of dom T : P₁[n,T . t] } \/ (dom T) as non empty set ;
M is Tree-like

thus M c= NAT * :: according to TREES_1:def 3 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in M ; :: thesis:
then A5: ( x in { (t ^ <*n*>) where n is Nat, t is Element of dom T : P₁[n,T . t] } or ( x in dom T & dom T c= NAT * ) ) by TREES_1:def 3, XBOOLE_0:def 3;
assume A6: not x in NAT * ; :: thesis:
then consider n being Nat, t being Element of dom T such that
A7: ( x = t ^ <*n*> & P₁[n,T . t] ) by A5;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
x = t ^ <*n*> by A7;
hence contradiction by A6, FINSEQ_1:def 11; :: thesis:

end;

thus for p being FinSequence of NAT st p in M holds
ProperPrefixes p c= M :: thesis:

let p be FinSequence of NAT ; :: thesis:
assume p in M ; :: thesis:
then A8: ( p in { (t ^ <*n*>) where n is Nat, t is Element of dom T : P₁[n,T . t] } or p in dom T ) by XBOOLE_0:def 3;

assume p in { (t ^ <*n*>) where n is Nat, t is Element of dom T : P₁[n,T . t] } ; :: thesis:
then consider n being Nat, t being Element of dom T such that
A9: p = t ^ <*n*> and
P₁[n,T . t] ;
A10: ProperPrefixes t c= dom T by TREES_1:def 3;
A11: dom T c= M by XBOOLE_1:7;
A12: ProperPrefixes t c= M by A10, A11;
A13: {t} c= M by A11, ZFMISC_1:31;
ProperPrefixes p = (ProperPrefixes t) \/ {t} by A9, Th4;
hence ProperPrefixes p c= M by A12, A13, XBOOLE_1:8; :: thesis:

end;

then ( ProperPrefixes p c= M or ( ProperPrefixes p c= dom T & dom T c= M ) ) by A8, TREES_1:def 3, XBOOLE_1:7;
hence ProperPrefixes p c= M ; :: thesis:

end;

let p be FinSequence of NAT ; :: thesis:
let m, n be Nat; :: thesis:
assume p ^ <*m*> in M ; :: thesis:
then A14: ( p ^ <*m*> in { (t ^ <*l*>) where l is Nat, t is Element of dom T : P₁[l,T . t] } or p ^ <*m*> in dom T ) by XBOOLE_0:def 3;
assume that
A15: n <= m and
A16: not p ^ <*n*> in M ; :: thesis:
not p ^ <*n*> in dom T by A16, XBOOLE_0:def 3;
then consider l being Nat, t being Element of dom T such that
A17: p ^ <*m*> = t ^ <*l*> and
A18: P₁[l,T . t] by A14, A15, TREES_1:def 3;
A19: ( len (p ^ <*m*>) = (len p) + (len <*m*>) & len <*m*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
A20: ( len (t ^ <*l*>) = (len t) + (len <*l*>) & len <*l*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
A21: ( (p ^ <*m*>) . ((len p) + 1) = m & (t ^ <*l*>) . ((len t) + 1) = l ) by FINSEQ_1:42;
then A22: p = t by A17, A19, A20, FINSEQ_1:33;
P₁[n,T . t] by A1, A15, A17, A18, A19, A20, A21;
then p ^ <*n*> in { (s ^ <*i*>) where i is Nat, s is Element of dom T : P₁[i,T . s] } by A22;
hence contradiction by A16, XBOOLE_0:def 3; :: thesis:

end;

then reconsider M = M as Tree ;
defpred S₂[ FinSequence, set ] means ( ( $1 in dom T & $2 = T . $1 ) or ( not $1 in dom T & ex n being Nat ex q being FinSequence of NAT st
( $1 = q ^ <*n*> & $2 = F₃() . ((T . q),n) ) ) );
A23: for p being FinSequence of NAT st p in M holds
ex x being set st S₂[p,x]

let p be FinSequence of NAT ; :: thesis:
assume p in M ; :: thesis:
then A24: ( p in { (t ^ <*l*>) where l is Nat, t is Element of dom T : P₁[l,T . t] } or p in dom T ) by XBOOLE_0:def 3;

assume A25: not p in dom T ; :: thesis:
then consider l being Nat, t being Element of dom T such that
A26: p = t ^ <*l*> and
P₁[l,T . t] by A24;
take x = F₃() . ((T . t),l); :: thesis:
thus ( ( p in dom T & x = T . p ) or ( not p in dom T & ex n being Nat ex q being FinSequence of NAT st
( p = q ^ <*n*> & x = F₃() . ((T . q),n) ) ) ) by A25, A26; :: thesis:

end;

hence ex x being set st S₂[p,x] ; :: thesis:

end;

consider T9 being DecoratedTree such that
A27: ( dom T9 = M & ( for p being FinSequence of NAT st p in M holds
S₂[p,T9 . p] ) ) from TREES_2:sch 6(A23);
rng T9 c= F₁()

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng T9 ; :: thesis:
then consider y being object such that
A28: y in dom T9 and
A29: x = T9 . y by FUNCT_1:def 3;
reconsider y = y as Element of dom T9 by A28;

A30: now :: thesis:

assume y in dom T ; :: thesis:
then reconsider t = y as Element of dom T ;
T . t in F₁() ;
hence x in F₁() by A27, A29; :: thesis:

end;

assume A31: not y in dom T ; :: thesis:
then consider n being Nat, q being FinSequence of NAT such that
A32: y = q ^ <*n*> and
A33: T9 . y = F₃() . ((T . q),n) by A27;
y in { (t ^ <*l*>) where l is Nat, t is Element of dom T : P₁[l,T . t] } by A27, A31, XBOOLE_0:def 3;
then consider l being Nat, t being Element of dom T such that
A34: y = t ^ <*l*> and
P₁[l,T . t] ;
A35: len <*n*> = 1 by FINSEQ_1:39;
A36: len <*l*> = 1 by FINSEQ_1:39;
A37: len (q ^ <*n*>) = (len q) + 1 by A35, FINSEQ_1:22;
A38: len (t ^ <*l*>) = (len t) + 1 by A36, FINSEQ_1:22;
( (q ^ <*n*>) . ((len q) + 1) = n & (t ^ <*l*>) . ((len t) + 1) = l ) by FINSEQ_1:42;
then A39: q = t by A32, A34, A37, A38, FINSEQ_1:33;
A40: n in NAT by ORDINAL1:def 12;
T . t in F₁() ;
then [(T . q),n] in [:F₁(),NAT:] by A39, ZFMISC_1:87, A40;
hence x in F₁() by A29, A33, FUNCT_2:5; :: thesis:

end;

hence x in F₁() by A30; :: thesis:

end;

then reconsider T9 = T9 as DecoratedTree of F₁() by RELAT_1:def 19;
take T9 ; :: thesis:
( <*> NAT in M & <*> NAT in dom T ) by TREES_1:22;
hence T9 . {} = F₂() by A4, A27; :: thesis:
let t be Element of dom T9; :: thesis:

A41: now :: thesis:

assume t in { (s ^ <*l*>) where l is Nat, s is Element of dom T : P₁[l,T . s] } ; :: thesis:
then consider l being Nat, s being Element of dom T such that
A42: t = s ^ <*l*> and
P₁[l,T . s] ;
len s <= k by A4;
then ( len <*l*> = 1 & (len s) + 1 <= k + 1 ) by FINSEQ_1:39, XREAL_1:7;
hence len t <= k + 1 by A42, FINSEQ_1:22; :: thesis:

end;

assume t in dom T ; :: thesis:
then reconsider s = t as Element of dom T ;
( len s <= k & k <= k + 1 ) by A4, NAT_1:11;
hence len t <= k + 1 by XXREAL_0:2; :: thesis:

end;

hence len t <= k + 1 by A27, A41, XBOOLE_0:def 3; :: thesis:
assume A43: len t < k + 1 ; :: thesis:

A44: now :: thesis:

assume A45: not t in dom T ; :: thesis:
then t in { (s ^ <*l*>) where l is Nat, s is Element of dom T : P₁[l,T . s] } by A27, XBOOLE_0:def 3;
then consider l being Nat, s being Element of dom T such that
A46: t = s ^ <*l*> and
A47: P₁[l,T . s] ;
A48: len t = (len s) + (len <*l*>) by A46, FINSEQ_1:22;
( len <*l*> = 1 & len t <= k ) by A43, FINSEQ_1:39, NAT_1:13;
then len s < k by A48, NAT_1:13;
then succ s = { (s ^ <*m*>) where m is Nat : P₁[m,T . s] } by A4;
then t in succ s by A46, A47;
hence contradiction by A45; :: thesis:

end;

then A49: T9 . t = T . t by A27;
reconsider t9 = t as Element of dom T by A44;
thus succ t c= { (t ^ <*i*>) where i is Nat : P₁[i,T9 . t] } :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in succ t ; :: thesis:
then consider n being Nat such that
A50: x = t ^ <*n*> and
A51: t ^ <*n*> in dom T9 ;

suppose A52: t ^ <*n*> in dom T ; :: thesis:

then reconsider s = t ^ <*n*>, t9 = t as Element of dom T by TREES_1:21;
( len s <= k & len s = (len t) + 1 ) by A4, FINSEQ_2:16;
then len t < k by NAT_1:13;
then succ t9 = { (t9 ^ <*m*>) where m is Nat : P₁[m,T . t9] } by A4;
hence x in { (t ^ <*i*>) where i is Nat : P₁[i,T9 . t] } by A49, A50, A52; :: thesis:

end;

suppose not t ^ <*n*> in dom T ; :: thesis:

then t ^ <*n*> in { (s ^ <*l*>) where l is Nat, s is Element of dom T : P₁[l,T . s] } by A27, A51, XBOOLE_0:def 3;
then consider l being Nat, s being Element of dom T such that
A53: t ^ <*n*> = s ^ <*l*> and
A54: P₁[l,T . s] ;
t = s by A53, FINSEQ_2:17;
hence x in { (t ^ <*i*>) where i is Nat : P₁[i,T9 . t] } by A49, A50, A53, A54; :: thesis:

end;

end;

end;

hence x in { (t ^ <*i*>) where i is Nat : P₁[i,T9 . t] } ; :: thesis:

end;

thus A55: { (t ^ <*i*>) where i is Nat : P₁[i,T9 . t] } c= succ t :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (t ^ <*i*>) where i is Nat : P₁[i,T9 . t] } ; :: thesis:
then consider n being Nat such that
A56: x = t ^ <*n*> and
A57: P₁[n,T9 . t] ;
x = t9 ^ <*n*> by A56;
then x in { (s ^ <*l*>) where l is Nat, s is Element of dom T : P₁[l,T . s] } by A49, A57;
then x in dom T9 by A27, XBOOLE_0:def 3;
hence x in succ t by A56; :: thesis:

end;

let n be Nat; :: thesis:
let x be set ; :: thesis:
assume that
A58: x = T9 . t and
A59: P₁[n,x] ; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 12;
t ^ <*n*> in { (t ^ <*i*>) where i is Nat : P₁[i,T9 . t] } by A58, A59;
then A60: t ^ <*n*> in succ t by A55;

suppose A61: t ^ <*n*> in dom T ; :: thesis:

then reconsider s = t ^ <*n*> as Element of dom T ;
( len s <= k & len s = (len t) + 1 ) by A4, FINSEQ_2:16;
then len t9 < k by NAT_1:13;
then T . (t9 ^ <*n*>) = F₃() . (x,n) by A4, A49, A58, A59;
hence T9 . (t ^ <*n*>) = F₃() . (x,n) by A27, A60, A61; :: thesis:

end;

suppose not t ^ <*n*> in dom T ; :: thesis:

then consider l being Nat, q being FinSequence of NAT such that
A62: t ^ <*n*> = q ^ <*l*> and
A63: T9 . (t ^ <*n*>) = F₃() . ((T . q),l) by A27, A60;
( t = q & n = l ) by A62, FINSEQ_2:17;
hence T9 . (t ^ <*n*>) = F₃() . (x,n) by A27, A44, A58, A63; :: thesis:

end;

end;

end;

hence T9 . (t ^ <*n*>) = F₃() . (x,n) ; :: thesis:

end;

A64: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
defpred S₂[ object , object ] means ex T being DecoratedTree of F₁() ex k being Nat st
( $1 = k & $2 = T & T . {} = F₂() & ( for t being Element of dom T holds
( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T . t] } & ( for n being Nat
for x being set st x = T . t & P₁[n,x] holds
T . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) );
A65: for x being object st x in NAT holds
ex y being object st S₂[x,y]

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Nat ;
consider T being DecoratedTree of F₁() such that
A66: ( T . {} = F₂() & ( for t being Element of dom T holds
( len t <= n & ( len t < n implies ( succ t = { (t ^ <*k*>) where k is Nat : P₁[k,T . t] } & ( for n being Nat
for x being set st x = T . t & P₁[n,x] holds
T . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A64;
reconsider y = T as set ;
take Y = y; :: thesis:
take T ; :: thesis:
take N = n; :: thesis:
thus ( x = N & Y = T & T . {} = F₂() & ( for t being Element of dom T holds
( len t <= N & ( len t < N implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T . t] } & ( for n being Nat
for x being set st x = T . t & P₁[n,x] holds
T . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A66; :: thesis:

end;

consider f being Function such that
A67: ( dom f = NAT & ( for x being object st x in NAT holds
S₂[x,f . x] ) ) from CLASSES1:sch 1(A65);
A68: for x being Nat holds S₂[x,f . x] by ORDINAL1:def 12, A67;
reconsider E = rng f as non empty set by A67, RELAT_1:42;
A69: for x being set st x in E holds
x is DecoratedTree of F₁()

let x be set ; :: thesis:
assume x in E ; :: thesis:
then consider y being object such that
A70: y in dom f and
A71: x = f . y by FUNCT_1:def 3;
ex T being DecoratedTree of F₁() ex k being Nat st
( y = k & f . y = T & T . {} = F₂() & ( for t being Element of dom T holds
( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T . t] } & ( for n being Nat
for x being set st x = T . t & P₁[n,x] holds
T . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A67, A70;
hence x is DecoratedTree of F₁() by A71; :: thesis:

end;

A72: for T1, T2 being DecoratedTree
for k1, k2 being Nat st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds
T1 c= T2

let T1, T2 be DecoratedTree; :: thesis:
let x, y be Nat; :: thesis:
assume that
A73: T1 = f . x and
A74: T2 = f . y and
A75: x <= y ; :: thesis:
consider T19 being DecoratedTree of F₁(), k1 being Nat such that
A76: ( x = k1 & f . x = T19 & T19 . {} = F₂() & ( for t being Element of dom T19 holds
( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T19 . t] } & ( for n being Nat
for x being set st x = T19 . t & P₁[n,x] holds
T19 . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A68;
consider T29 being DecoratedTree of F₁(), k2 being Nat such that
A77: ( y = k2 & f . y = T29 & T29 . {} = F₂() & ( for t being Element of dom T29 holds
( len t <= k2 & ( len t < k2 implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T29 . t] } & ( for n being Nat
for x being set st x = T29 . t & P₁[n,x] holds
T29 . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A68;
defpred S₃[ Nat] means for t being Element of dom T1 st len t <= $1 holds
( t in dom T2 & T1 . t = T2 . t );
A78: S₃[ 0 ]

let t be Element of dom T1; :: thesis:
assume A79: len t <= 0 ; :: thesis:
t = {} by A79;
hence ( t in dom T2 & T1 . t = T2 . t ) by A73, A74, A76, A77, TREES_1:22; :: thesis:

end;

A80: for k being Nat st S₃[k] holds
S₃[k + 1]

let k be Nat; :: thesis:
assume A81: for t being Element of dom T1 st len t <= k holds
( t in dom T2 & T1 . t = T2 . t ) ; :: thesis:
let t be Element of dom T1; :: thesis:
assume len t <= k + 1 ; :: thesis:
then A82: ( len t <= k or len t = k + 1 ) by NAT_1:8;

assume A83: len t = k + 1 ; :: thesis:
reconsider p = t | (Seg k) as FinSequence of NAT by FINSEQ_1:18;
p is_a_prefix_of t ;
then reconsider p = p as Element of dom T1 by TREES_1:20;
A84: k <= k + 1 by NAT_1:11;
A85: k + 1 <= k1 by A73, A76, A83;
A86: len p = k by A83, A84, FINSEQ_1:17;
A87: k < k1 by A85, NAT_1:13;
A88: T1 . p = T2 . p by A81, A86;
reconsider p9 = p as Element of dom T2 by A81, A86;
t <> {} by A83;
then consider q being FinSequence, x being object such that
A89: t = q ^ <*x*> by FINSEQ_1:46;
A90: ( p is_a_prefix_of t & q is_a_prefix_of t ) by A89, TREES_1:1;
k + 1 = (len q) + 1 by A83, A89, FINSEQ_2:16;
then A91: p = q by A86, A90, Th1, TREES_1:4;
<*x*> is FinSequence of NAT by A89, FINSEQ_1:36;
then A92: rng <*x*> c= NAT by FINSEQ_1:def 4;
( rng <*x*> = {x} & x in {x} ) by FINSEQ_1:38, TARSKI:def 1;
then reconsider x = x as Nat by A92;
A93: p ^ <*x*> in succ p by A89, A91;
succ p = { (p ^ <*i*>) where i is Nat : P₁[i,T1 . p] } by A73, A76, A86, A87;
then consider i being Nat such that
A94: p ^ <*x*> = p ^ <*i*> and
A95: P₁[i,T1 . p] by A93;
A96: k < k2 by A75, A76, A77, A87, XXREAL_0:2;
then A97: succ p9 = { (p9 ^ <*l*>) where l is Nat : P₁[l,T2 . p9] } by A74, A77, A86;
A98: x = i by A94, FINSEQ_2:17;
A99: t in succ p9 by A88, A89, A91, A94, A95, A97;
T19 . t = F₃() . ((T19 . p),x) by A73, A76, A86, A87, A89, A91, A95, A98;
hence ( t in dom T2 & T1 . t = T2 . t ) by A73, A74, A76, A77, A86, A88, A89, A91, A95, A96, A98, A99; :: thesis:

end;

hence ( t in dom T2 & T1 . t = T2 . t ) by A81, A82; :: thesis:

end;

A100: for k being Nat holds S₃[k] from NAT_1:sch 2(A78, A80);
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A101: x in T1 ; :: thesis:
then consider y, z being object such that
A102: [y,z] = x by RELAT_1:def 1;
A103: T1 . y = z by A101, A102, FUNCT_1:1;
reconsider y = y as Element of dom T1 by A101, A102, FUNCT_1:1;
len y <= len y ;
then ( y in dom T2 & T1 . y = T2 . y ) by A100;
hence x in T2 by A102, A103, FUNCT_1:1; :: thesis:

end;

let T1, T2 be set ; :: according to ORDINAL1:def 8 :: thesis:
assume A104: T1 in E ; :: thesis:
then consider x being object such that
A105: x in dom f and
A106: T1 = f . x by FUNCT_1:def 3;
assume A107: T2 in E ; :: thesis:
then consider y being object such that
A108: y in dom f and
A109: T2 = f . y by FUNCT_1:def 3;
A110: T1 is DecoratedTree by A69, A104;
A111: T2 is DecoratedTree by A69, A107;
reconsider x = x, y = y as Nat by A67, A105, A108;
( x <= y or y <= x ) ;
hence ( T1 c= T2 or T2 c= T1 ) by A72, A106, A109, A110, A111; :: according to XBOOLE_0:def 9 :: thesis:

end;

then reconsider T = union (rng f) as DecoratedTree of F₁() by A69, Th36;
take T ; :: thesis:
consider T9 being DecoratedTree of F₁(), k being Nat such that
A112: ( 0 = k & f . 0 = T9 & T9 . {} = F₂() & ( for t being Element of dom T9 holds
( len t <= k & ( len t < k implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T9 . t] } & ( for n being Nat
for x being set st x = T9 . t & P₁[n,x] holds
T9 . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A67;
{} in dom T9 by TREES_1:22;
then A113: [{},F₂()] in T9 by A112, FUNCT_1:1;
T9 in rng f by A67, A112, FUNCT_1:def 3;
then [{},F₂()] in T by A113, TARSKI:def 4;
hence T . {} = F₂() by FUNCT_1:1; :: thesis:
A114: for T1 being DecoratedTree
for x being set st T1 in E & x in dom T1 holds
( x in dom T & T1 . x = T . x )

let T1 be DecoratedTree; :: thesis:
let x be set ; :: thesis:
assume that
A115: T1 in E and
A116: x in dom T1 ; :: thesis:
[x,(T1 . x)] in T1 by A116, FUNCT_1:1;
then [x,(T1 . x)] in T by A115, TARSKI:def 4;
hence ( x in dom T & T1 . x = T . x ) by FUNCT_1:1; :: thesis:

end;

let t be Element of dom T; :: thesis:
thus succ t c= { (t ^ <*i*>) where i is Nat : P₁[i,T . t] } :: according to XBOOLE_0:def 10 :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in succ t ; :: thesis:
then consider l being Nat such that
A117: x = t ^ <*l*> and
A118: t ^ <*l*> in dom T ;
[x,(T . x)] in T by A117, A118, FUNCT_1:1;
then consider X being set such that
A119: [x,(T . x)] in X and
A120: X in rng f by TARSKI:def 4;
consider y being object such that
A121: y in NAT and
A122: X = f . y by A67, A120, FUNCT_1:def 3;
consider T1 being DecoratedTree of F₁(), k1 being Nat such that
A123: ( y = k1 & f . y = T1 & T1 . {} = F₂() & ( for t being Element of dom T1 holds
( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T1 . t] } & ( for n being Nat
for x being set st x = T1 . t & P₁[n,x] holds
T1 . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A67, A121;
A124: t ^ <*l*> in dom T1 by A117, A119, A122, A123, FUNCT_1:1;
then reconsider t9 = t, p = t ^ <*l*> as Element of dom T1 by TREES_1:21;
len p <= k1 by A123;
then (len t) + 1 <= k1 by FINSEQ_2:16;
then A125: len t9 < k1 by NAT_1:13;
then A126: succ t9 = { (t9 ^ <*i*>) where i is Nat : P₁[i,T1 . t9] } by A123;
T1 . t = T . t by A114, A120, A122, A123, A125;
hence x in { (t ^ <*i*>) where i is Nat : P₁[i,T . t] } by A117, A124, A126; :: thesis:

end;

[t,(T . t)] in T by FUNCT_1:1;
then consider X being set such that
A127: [t,(T . t)] in X and
A128: X in E by TARSKI:def 4;
consider y being object such that
A129: y in NAT and
A130: X = f . y by A67, A128, FUNCT_1:def 3;
reconsider y = y as Nat by A129;
consider T1 being DecoratedTree of F₁(), k1 being Nat such that
A131: ( y = k1 & f . y = T1 & T1 . {} = F₂() & ( for t being Element of dom T1 holds
( len t <= k1 & ( len t < k1 implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T1 . t] } & ( for n being Nat
for x being set st x = T1 . t & P₁[n,x] holds
T1 . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A68;
consider T2 being DecoratedTree of F₁(), k2 being Nat such that
A132: ( y + 1 = k2 & f . (y + 1) = T2 & T2 . {} = F₂() & ( for t being Element of dom T2 holds
( len t <= k2 & ( len t < k2 implies ( succ t = { (t ^ <*i*>) where i is Nat : P₁[i,T2 . t] } & ( for n being Nat
for x being set st x = T2 . t & P₁[n,x] holds
T2 . (t ^ <*n*>) = F₃() . (x,n) ) ) ) ) ) ) by A67;
y <= y + 1 by NAT_1:11;
then A133: T1 c= T2 by A72, A131, A132;
reconsider t1 = t as Element of dom T1 by A127, A130, A131, FUNCT_1:1;
A134: len t1 <= y by A131;
A135: T2 . t = T . t by A127, A130, A131, A133, FUNCT_1:1;
reconsider t2 = t as Element of dom T2 by A127, A130, A131, A133, FUNCT_1:1;
A136: len t2 < y + 1 by A134, NAT_1:13;
then A137: succ t2 = { (t2 ^ <*i*>) where i is Nat : P₁[i,T2 . t2] } by A132;
thus { (t ^ <*i*>) where i is Nat : P₁[i,T . t] } c= succ t :: thesis:

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A138: x in { (t ^ <*i*>) where i is Nat : P₁[i,T . t] } ; :: thesis:
then A139: ex l being Nat st
( x = t ^ <*l*> & P₁[l,T . t] ) ;
A140: x in succ t2 by A132, A135, A136, A138;
T2 in E by A67, A132, FUNCT_1:def 3;
then x in dom T by A114, A140;
hence x in succ t by A139; :: thesis:

end;

let n be Nat; :: thesis:
assume A141: P₁[n,T . t] ; :: thesis:
then A142: t ^ <*n*> in succ t2 by A135, A137;
T2 in E by A67, A132, FUNCT_1:def 3;
then T2 . (t ^ <*n*>) = T . (t ^ <*n*>) by A114, A142;
hence T . (t ^ <*n*>) = F₃() . ((T . t),n) by A132, A135, A136, A141; :: thesis: