defpred S₁[ Element of 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 Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) );
A2: S₁[ 0 ]

proof

reconsider W = {{}} as Tree ;
take T = W --> F₂(); :: thesis: ( T . {} = F₂() & ( for t being Element of dom T holds
( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) )
{} in W by TREES_1:22;
hence T . {} = F₂() by FUNCOP_1:7; :: thesis: for t being Element of dom T holds
( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) )
let t be Element of dom T; :: thesis: ( len t <= 0 & ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) )
dom T = W by FUNCOP_1:13;
then t = {} by TARSKI:def 1;
hence len t <= 0 ; :: thesis: ( len t < 0 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) )
assume len t < 0 ; :: thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) )
hence ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ; :: thesis: verum

end;

A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
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 Element of NAT : m in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) ; :: thesis: S₁[k + 1]
reconsider M = { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : n in F₃((T . t)) } \/ (dom T) as non empty set ;
M is Tree-like

proof

thus M c= NAT * :: according to TREES_1:def 3 :: thesis: ( ( for b₁ being FinSequence of NAT holds
( not b₁ in M or ProperPrefixes b₁ c= M ) ) & ( for b₁ being FinSequence of NAT
for b₂, b₃ being Element of NAT holds
( not b₁ ^ <*b₂*> in M or not b₃ <= b₂ or b₁ ^ <*b₃*> in M ) ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in M or x in NAT * )
assume x in M ; :: thesis: x in NAT *
then A5: ( x in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : n in F₃((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: contradiction
then ex n being Element of NAT ex t being Element of dom T st
( x = t ^ <*n*> & n in F₃((T . t)) ) by A5;
hence contradiction by A6, FINSEQ_1:def 11; :: thesis: verum

end;

thus for p being FinSequence of NAT st p in M holds
ProperPrefixes p c= M :: thesis: for b₁ being FinSequence of NAT
for b₂, b₃ being Element of NAT holds
( not b₁ ^ <*b₂*> in M or not b₃ <= b₂ or b₁ ^ <*b₃*> in M )

proof

let p be FinSequence of NAT ; :: thesis: ( p in M implies ProperPrefixes p c= M )
assume p in M ; :: thesis: ProperPrefixes p c= M
then A7: ( p in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : n in F₃((T . t)) } or p in dom T ) by XBOOLE_0:def 3;

now

assume p in { (t ^ <*n*>) where n is Element of NAT , t is Element of dom T : n in F₃((T . t)) } ; :: thesis: ProperPrefixes p c= M
then consider n being Element of NAT , t being Element of dom T such that
A8: p = t ^ <*n*> and
n in F₃((T . t)) ;
A9: ProperPrefixes t c= dom T by TREES_1:def 3;
A10: dom T c= M by XBOOLE_1:7;
A11: t in dom T ;
A12: ProperPrefixes t c= M by A9, A10, XBOOLE_1:1;
A13: {t} c= M by A10, A11, ZFMISC_1:31;
ProperPrefixes p = (ProperPrefixes t) \/ {t} by A8, Th6;
hence ProperPrefixes p c= M by A12, A13, XBOOLE_1:8; :: thesis: verum

end;

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

end;

let p be FinSequence of NAT ; :: thesis: for b₁, b₂ being Element of NAT holds
( not p ^ <*b₁*> in M or not b₂ <= b₁ or p ^ <*b₂*> in M )
let m, n be Element of NAT ; :: thesis: ( not p ^ <*m*> in M or not n <= m or p ^ <*n*> in M )
assume p ^ <*m*> in M ; :: thesis: ( not n <= m or p ^ <*n*> in M )
then A14: ( p ^ <*m*> in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : l in F₃((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: contradiction
not p ^ <*n*> in dom T by A16, XBOOLE_0:def 3;
then consider l being Element of NAT , t being Element of dom T such that
A17: p ^ <*m*> = t ^ <*l*> and
A18: l in F₃((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;
n in F₃((T . t)) by A1, A15, A17, A18, A19, A20, A21;
then p ^ <*n*> in { (s ^ <*i*>) where i is Element of NAT , s is Element of dom T : i in F₃((T . s)) } by A22;
hence contradiction by A16, XBOOLE_0:def 3; :: thesis: verum

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 Element of 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]

proof

let p be FinSequence of NAT ; :: thesis: ( p in M implies ex x being set st S₂[p,x] )
assume p in M ; :: thesis: ex x being set st S₂[p,x]
then A24: ( p in { (t ^ <*l*>) where l is Element of NAT , t is Element of dom T : l in F₃((T . t)) } or p in dom T ) by XBOOLE_0:def 3;

now

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

end;

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

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₁()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng T9 or x in F₁() )
assume x in rng T9 ; :: thesis: x in F₁()
then consider y being set 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

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

end;

now

assume A31: not y in dom T ; :: thesis: x in F₁()
then consider n being Element of 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 Element of NAT , t is Element of dom T : l in F₃((T . t)) } by A27, A31, XBOOLE_0:def 3;
then consider l being Element of NAT , t being Element of dom T such that
A34: y = t ^ <*l*> and
l in F₃((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;
T . t in F₁() ;
then [(T . q),n] in [:F₁(),NAT:] by A39, ZFMISC_1:87;
hence x in F₁() by A29, A33, FUNCT_2:5; :: thesis: verum

end;

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

end;

then reconsider T9 = T9 as DecoratedTree of F₁() by RELAT_1:def 19;
take T9 ; :: thesis: ( T9 . {} = F₂() & ( for t being Element of dom T9 holds
( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T9 . t)) } & ( for n being Element of NAT
for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) )
( <*> NAT in M & <*> NAT in dom T ) by TREES_1:22;
hence T9 . {} = F₂() by A4, A27; :: thesis: for t being Element of dom T9 holds
( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T9 . t)) } & ( for n being Element of NAT
for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) )
let t be Element of dom T9; :: thesis: ( len t <= k + 1 & ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T9 . t)) } & ( for n being Element of NAT
for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) )

A40: now

assume t in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : l in F₃((T . s)) } ; :: thesis: len t <= k + 1
then consider l being Element of NAT , s being Element of dom T such that
A41: t = s ^ <*l*> and
l in F₃((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 A41, FINSEQ_1:22; :: thesis: verum

end;

now

assume t in dom T ; :: thesis: len t <= k + 1
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: verum

end;

hence len t <= k + 1 by A27, A40, XBOOLE_0:def 3; :: thesis: ( len t < k + 1 implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T9 . t)) } & ( for n being Element of NAT
for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n) ) ) )
assume A42: len t < k + 1 ; :: thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T9 . t)) } & ( for n being Element of NAT
for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n) ) )

A43: now

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

end;

then A48: T9 . t = T . t by A27;
reconsider t9 = t as Element of dom T by A43;
thus succ t c= { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } :: according to XBOOLE_0:def 10 :: thesis: ( { (t ^ <*k*>) where k is Element of NAT : k in F₃((T9 . t)) } c= succ t & ( for n being Element of NAT
for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n) ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } )
assume x in succ t ; :: thesis: x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) }
then consider n being Element of NAT such that
A49: x = t ^ <*n*> and
A50: t ^ <*n*> in dom T9 ;

now

per cases ( t ^ <*n*> in dom T or not t ^ <*n*> in dom T ) ;

suppose A51: t ^ <*n*> in dom T ; :: thesis: x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) }

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 Element of NAT : m in F₃((T . t9)) } by A4;
hence x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } by A48, A49, A51; :: thesis: verum

end;

suppose not t ^ <*n*> in dom T ; :: thesis: x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) }

then t ^ <*n*> in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : l in F₃((T . s)) } by A27, A50, XBOOLE_0:def 3;
then consider l being Element of NAT , s being Element of dom T such that
A52: t ^ <*n*> = s ^ <*l*> and
A53: l in F₃((T . s)) ;
t = s by A52, FINSEQ_2:17;
hence x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } by A48, A49, A52, A53; :: thesis: verum

end;

end;

end;

hence x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } ; :: thesis: verum

end;

thus A54: { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } c= succ t :: thesis: for n being Element of NAT
for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } or x in succ t )
assume x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } ; :: thesis: x in succ t
then consider n being Element of NAT such that
A55: x = t ^ <*n*> and
A56: n in F₃((T9 . t)) ;
x = t9 ^ <*n*> by A55;
then x in { (s ^ <*l*>) where l is Element of NAT , s is Element of dom T : l in F₃((T . s)) } by A48, A56;
then x in dom T9 by A27, XBOOLE_0:def 3;
hence x in succ t by A55; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n)
let x be set ; :: thesis: ( x = T9 . t & n in F₃(x) implies T9 . (t ^ <*n*>) = F₄() . (x,n) )
assume that
A57: x = T9 . t and
A58: n in F₃(x) ; :: thesis: T9 . (t ^ <*n*>) = F₄() . (x,n)
t ^ <*n*> in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T9 . t)) } by A57, A58;
then A59: t ^ <*n*> in succ t by A54;

now

per cases ( t ^ <*n*> in dom T or not t ^ <*n*> in dom T ) ;

suppose A60: t ^ <*n*> in dom T ; :: thesis: T9 . (t ^ <*n*>) = F₄() . (x,n)

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, A48, A57, A58;
hence T9 . (t ^ <*n*>) = F₄() . (x,n) by A27, A59, A60; :: thesis: verum

end;

suppose not t ^ <*n*> in dom T ; :: thesis: T9 . (t ^ <*n*>) = F₄() . (x,n)

then consider l being Element of NAT , q being FinSequence of NAT such that
A61: t ^ <*n*> = q ^ <*l*> and
A62: T9 . (t ^ <*n*>) = F₄() . ((T . q),l) by A27, A59;
( t = q & n = l ) by A61, FINSEQ_2:17;
hence T9 . (t ^ <*n*>) = F₄() . (x,n) by A27, A43, A57, A62; :: thesis: verum

end;

end;

end;

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

end;

A63: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);
defpred S₂[ set , set ] means ex T being DecoratedTree of F₁() ex k being Element of 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 Element of NAT : i in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) );
A64: for x being set st x in NAT holds
ex y being set st S₂[x,y]

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st S₂[x,y] )
assume x in NAT ; :: thesis: ex y being set st S₂[x,y]
then reconsider n = x as Element of NAT ;
consider T being DecoratedTree of F₁() such that
A65: ( T . {} = F₂() & ( for t being Element of dom T holds
( len t <= n & ( len t < n implies ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A63;
reconsider y = T as set ;
take y ; :: thesis: S₂[x,y]
take T ; :: thesis: ex k being Element of NAT st
( x = k & 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 Element of NAT : i in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) )
take n ; :: thesis: ( 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 Element of NAT : i in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) )
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 Element of NAT : i in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A65; :: thesis: verum

end;

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

proof

let x be set ; :: thesis: ( x in E implies x is DecoratedTree of F₁() )
assume x in E ; :: thesis: x is DecoratedTree of F₁()
then consider y being set such that
A68: y in dom f and
A69: x = f . y by FUNCT_1:def 3;
ex T being DecoratedTree of F₁() ex k being Element of 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 Element of NAT : i in F₃((T . t)) } & ( for n being Element of NAT
for x being set st x = T . t & n in F₃(x) holds
T . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A66, A68;
hence x is DecoratedTree of F₁() by A69; :: thesis: verum

end;

A70: for T1, T2 being DecoratedTree
for k1, k2 being Element of NAT st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds
T1 c= T2

proof

let T1, T2 be DecoratedTree; :: thesis: for k1, k2 being Element of NAT st T1 = f . k1 & T2 = f . k2 & k1 <= k2 holds
T1 c= T2
let x, y be Element of NAT ; :: thesis: ( T1 = f . x & T2 = f . y & x <= y implies T1 c= T2 )
assume that
A71: T1 = f . x and
A72: T2 = f . y and
A73: x <= y ; :: thesis: T1 c= T2
consider T19 being DecoratedTree of F₁(), k1 being Element of NAT such that
A74: ( 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 Element of NAT : i in F₃((T19 . t)) } & ( for n being Element of NAT
for x being set st x = T19 . t & n in F₃(x) holds
T19 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A66;
consider T29 being DecoratedTree of F₁(), k2 being Element of NAT such that
A75: ( 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 Element of NAT : i in F₃((T29 . t)) } & ( for n being Element of NAT
for x being set st x = T29 . t & n in F₃(x) holds
T29 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A66;
defpred S₃[ Element of NAT ] means for t being Element of dom T1 st len t <= $1 holds
( t in dom T2 & T1 . t = T2 . t );
A76: S₃[ 0 ]

proof

let t be Element of dom T1; :: thesis: ( len t <= 0 implies ( t in dom T2 & T1 . t = T2 . t ) )
assume A77: len t <= 0 ; :: thesis: ( t in dom T2 & T1 . t = T2 . t )
t = {} by A77;
hence ( t in dom T2 & T1 . t = T2 . t ) by A71, A72, A74, A75, TREES_1:22; :: thesis: verum

end;

A78: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₃[k] implies S₃[k + 1] )
assume A79: for t being Element of dom T1 st len t <= k holds
( t in dom T2 & T1 . t = T2 . t ) ; :: thesis: S₃[k + 1]
let t be Element of dom T1; :: thesis: ( len t <= k + 1 implies ( t in dom T2 & T1 . t = T2 . t ) )
assume len t <= k + 1 ; :: thesis: ( t in dom T2 & T1 . t = T2 . t )
then A80: ( len t <= k or len t = k + 1 ) by NAT_1:8;

now

assume A81: len t = k + 1 ; :: thesis: ( t in dom T2 & T1 . t = T2 . t )
reconsider p = t | (Seg k) as FinSequence of NAT by FINSEQ_1:18;
p is_a_prefix_of t by TREES_1:def 1;
then reconsider p = p as Element of dom T1 by TREES_1:20;
A82: k <= k + 1 by NAT_1:11;
A83: k + 1 <= k1 by A71, A74, A81;
A84: len p = k by A81, A82, FINSEQ_1:17;
A85: k < k1 by A83, NAT_1:13;
A86: T1 . p = T2 . p by A79, A84;
reconsider p9 = p as Element of dom T2 by A79, A84;
t <> {} by A81;
then consider q being FinSequence, x being set such that
A87: t = q ^ <*x*> by FINSEQ_1:46;
A88: ( p is_a_prefix_of t & q is_a_prefix_of t ) by A87, TREES_1:1, TREES_1:def 1;
k + 1 = (len q) + 1 by A81, A87, FINSEQ_2:16;
then A89: p = q by A84, A88, Th1, TREES_1:4;
<*x*> is FinSequence of NAT by A87, FINSEQ_1:36;
then A90: 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 Element of NAT by A90;
A91: p ^ <*x*> in succ p by A87, A89;
succ p = { (p ^ <*i*>) where i is Element of NAT : i in F₃((T1 . p)) } by A71, A74, A84, A85;
then consider i being Element of NAT such that
A92: p ^ <*x*> = p ^ <*i*> and
A93: i in F₃((T1 . p)) by A91;
A94: k < k2 by A73, A74, A75, A85, XXREAL_0:2;
then A95: succ p9 = { (p9 ^ <*l*>) where l is Element of NAT : l in F₃((T2 . p9)) } by A72, A75, A84;
A96: x = i by A92, FINSEQ_2:17;
A97: t in succ p9 by A86, A87, A89, A92, A93, A95;
T19 . t = F₄() . ((T19 . p),x) by A71, A74, A84, A85, A87, A89, A93, A96;
hence ( t in dom T2 & T1 . t = T2 . t ) by A71, A72, A74, A75, A84, A86, A87, A89, A93, A94, A96, A97; :: thesis: verum

end;

hence ( t in dom T2 & T1 . t = T2 . t ) by A79, A80; :: thesis: verum

end;

A98: for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A76, A78);
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in T1 or x in T2 )
assume A99: x in T1 ; :: thesis: x in T2
then consider y, z being set such that
A100: [y,z] = x by RELAT_1:def 1;
A101: T1 . y = z by A99, A100, FUNCT_1:1;
reconsider y = y as Element of dom T1 by A99, A100, FUNCT_1:1;
len y <= len y ;
then ( y in dom T2 & T1 . y = T2 . y ) by A98;
hence x in T2 by A100, A101, FUNCT_1:1; :: thesis: verum

end;

E is c=-linear

proof

let T1, T2 be set ; :: according to ORDINAL1:def 8 :: thesis: ( not T1 in E or not T2 in E or T1,T2 are_c=-comparable )
assume A102: T1 in E ; :: thesis: ( not T2 in E or T1,T2 are_c=-comparable )
then consider x being set such that
A103: x in dom f and
A104: T1 = f . x by FUNCT_1:def 3;
assume A105: T2 in E ; :: thesis: T1,T2 are_c=-comparable
then consider y being set such that
A106: y in dom f and
A107: T2 = f . y by FUNCT_1:def 3;
A108: T1 is DecoratedTree by A67, A102;
A109: T2 is DecoratedTree by A67, A105;
reconsider x = x, y = y as Element of NAT by A66, A103, A106;
( x <= y or y <= x ) ;
hence ( T1 c= T2 or T2 c= T1 ) by A70, A104, A107, A108, A109; :: according to XBOOLE_0:def 9 :: thesis: verum

end;

then reconsider T = union (rng f) as DecoratedTree of F₁() by A67, Th38;
take T ; :: thesis: ( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT st n in F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) ) ) )
consider T9 being DecoratedTree of F₁(), k being Element of NAT such that
A110: ( 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 Element of NAT : i in F₃((T9 . t)) } & ( for n being Element of NAT
for x being set st x = T9 . t & n in F₃(x) holds
T9 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A66;
{} in dom T9 by TREES_1:22;
then A111: [{},F₂()] in T9 by A110, FUNCT_1:1;
T9 in rng f by A66, A110, FUNCT_1:def 3;
then [{},F₂()] in T by A111, TARSKI:def 4;
hence T . {} = F₂() by FUNCT_1:1; :: thesis: for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT st n in F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) )
A112: 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 )

proof

let T1 be DecoratedTree; :: thesis: for x being set st T1 in E & x in dom T1 holds
( x in dom T & T1 . x = T . x )
let x be set ; :: thesis: ( T1 in E & x in dom T1 implies ( x in dom T & T1 . x = T . x ) )
assume that
A113: T1 in E and
A114: x in dom T1 ; :: thesis: ( x in dom T & T1 . x = T . x )
[x,(T1 . x)] in T1 by A114, FUNCT_1:1;
then [x,(T1 . x)] in T by A113, TARSKI:def 4;
hence ( x in dom T & T1 . x = T . x ) by FUNCT_1:1; :: thesis: verum

end;

let t be Element of dom T; :: thesis: ( succ t = { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } & ( for n being Element of NAT st n in F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) )
thus succ t c= { (t ^ <*i*>) where i is Element of NAT : i in F₃((T . t)) } :: according to XBOOLE_0:def 10 :: thesis: ( { (t ^ <*k*>) where k is Element of NAT : k in F₃((T . t)) } c= succ t & ( for n being Element of NAT st n in F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n) ) )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ t or x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T . t)) } )
assume x in succ t ; :: thesis: x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T . t)) }
then consider l being Element of NAT such that
A115: x = t ^ <*l*> and
A116: t ^ <*l*> in dom T ;
[x,(T . x)] in T by A115, A116, FUNCT_1:1;
then consider X being set such that
A117: [x,(T . x)] in X and
A118: X in rng f by TARSKI:def 4;
consider y being set such that
A119: y in NAT and
A120: X = f . y by A66, A118, FUNCT_1:def 3;
consider T1 being DecoratedTree of F₁(), k1 being Element of NAT such that
A121: ( 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 Element of NAT : i in F₃((T1 . t)) } & ( for n being Element of NAT
for x being set st x = T1 . t & n in F₃(x) holds
T1 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A66, A119;
A122: t ^ <*l*> in dom T1 by A115, A117, A120, A121, FUNCT_1:1;
then reconsider t9 = t, p = t ^ <*l*> as Element of dom T1 by TREES_1:21;
len p <= k1 by A121;
then (len t) + 1 <= k1 by FINSEQ_2:16;
then A123: len t9 < k1 by NAT_1:13;
then A124: succ t9 = { (t9 ^ <*i*>) where i is Element of NAT : i in F₃((T1 . t9)) } by A121;
T1 . t = T . t by A112, A118, A120, A121, A123;
hence x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T . t)) } by A115, A122, A124; :: thesis: verum

end;

[t,(T . t)] in T by FUNCT_1:1;
then consider X being set such that
A125: [t,(T . t)] in X and
A126: X in E by TARSKI:def 4;
consider y being set such that
A127: y in NAT and
A128: X = f . y by A66, A126, FUNCT_1:def 3;
reconsider y = y as Element of NAT by A127;
consider T1 being DecoratedTree of F₁(), k1 being Element of NAT such that
A129: ( 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 Element of NAT : i in F₃((T1 . t)) } & ( for n being Element of NAT
for x being set st x = T1 . t & n in F₃(x) holds
T1 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A66;
consider T2 being DecoratedTree of F₁(), k2 being Element of NAT such that
A130: ( 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 Element of NAT : i in F₃((T2 . t)) } & ( for n being Element of NAT
for x being set st x = T2 . t & n in F₃(x) holds
T2 . (t ^ <*n*>) = F₄() . (x,n) ) ) ) ) ) ) by A66;
y <= y + 1 by NAT_1:11;
then A131: T1 c= T2 by A70, A129, A130;
reconsider t1 = t as Element of dom T1 by A125, A128, A129, FUNCT_1:1;
A132: len t1 <= y by A129;
A133: T2 . t = T . t by A125, A128, A129, A131, FUNCT_1:1;
reconsider t2 = t as Element of dom T2 by A125, A128, A129, A131, FUNCT_1:1;
A134: len t2 < y + 1 by A132, NAT_1:13;
then A135: succ t2 = { (t2 ^ <*i*>) where i is Element of NAT : i in F₃((T2 . t2)) } by A130;
thus { (t ^ <*i*>) where i is Element of NAT : i in F₃((T . t)) } c= succ t :: thesis: for n being Element of NAT st n in F₃((T . t)) holds
T . (t ^ <*n*>) = F₄() . ((T . t),n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T . t)) } or x in succ t )
assume A136: x in { (t ^ <*i*>) where i is Element of NAT : i in F₃((T . t)) } ; :: thesis: x in succ t
then A137: ex l being Element of NAT st
( x = t ^ <*l*> & l in F₃((T . t)) ) ;
A138: x in succ t2 by A130, A133, A134, A136;
T2 in E by A66, A130, FUNCT_1:def 3;
then x in dom T by A112, A138;
hence x in succ t by A137; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( n in F₃((T . t)) implies T . (t ^ <*n*>) = F₄() . ((T . t),n) )
assume A139: n in F₃((T . t)) ; :: thesis: T . (t ^ <*n*>) = F₄() . ((T . t),n)
then A140: t ^ <*n*> in succ t2 by A133, A135;
T2 in E by A66, A130, FUNCT_1:def 3;
then T2 . (t ^ <*n*>) = T . (t ^ <*n*>) by A112, A140;
hence T . (t ^ <*n*>) = F₄() . ((T . t),n) by A130, A133, A134, A139; :: thesis: verum