defpred S₁[ set , set ] means ( ( len F₃($1) = 0 & $2 = {} ) or ( len F₃($1) <> 0 & ex m being Element of NAT st
( m + 1 = len F₃($1) & $2 = {0 } \/ (Seg m) ) ) );
A2: for x being set st x in F₁() holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in F₁() implies ex y being set st S₁[x,y] )
assume x in F₁() ; :: thesis: ex y being set st S₁[x,y]

per cases ( len F₃(x) = 0 or len F₃(x) <> 0 ) ;

suppose len F₃(x) = 0 ; :: thesis: ex y being set st S₁[x,y]

hence ex y being set st S₁[x,y] ; :: thesis: verum

end;

suppose len F₃(x) <> 0 ; :: thesis: ex y being set st S₁[x,y]

then consider m being Nat such that
A3: m + 1 = len F₃(x) by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
ex y being set st y = {0 } \/ (Seg m) ;
hence ex y being set st S₁[x,y] by A3; :: thesis: verum

end;

end;

end;

ex F being Function st
( dom F = F₁() & ( for x being set st x in F₁() holds
S₁[x,F . x] ) ) from CLASSES1:sch 1(A2);
then consider F being Function such that
A4: for x being set holds
( not x in F₁() or ( len F₃(x) = 0 & F . x = {} ) or ( len F₃(x) <> 0 & ex m being Element of NAT st
( m + 1 = len F₃(x) & F . x = {0 } \/ (Seg m) ) ) ) ;
deffunc H₁( set ) -> set = F . $1;
A5: for k being Element of NAT
for x being set st x in F₁() holds
( k in H₁(x) iff k + 1 in Seg (len F₃(x)) )

proof

let k be Element of NAT ; :: thesis: for x being set st x in F₁() holds
( k in H₁(x) iff k + 1 in Seg (len F₃(x)) )
let x be set ; :: thesis: ( x in F₁() implies ( k in H₁(x) iff k + 1 in Seg (len F₃(x)) ) )
assume A6: x in F₁() ; :: thesis: ( k in H₁(x) iff k + 1 in Seg (len F₃(x)) )

now

assume A7: k in H₁(x) ; :: thesis: k + 1 in Seg (len F₃(x))
then consider m being Element of NAT such that
A8: ( m + 1 = len F₃(x) & F . x = {0 } \/ (Seg m) ) by A4, A6;
( 0 <= k & k <= m )

proof

per cases ( k in {0 } or k in Seg m ) by A7, A8, XBOOLE_0:def 3;

suppose k in {0 } ; :: thesis: ( 0 <= k & k <= m )

then k = 0 by TARSKI:def 1;
hence ( 0 <= k & k <= m ) by NAT_1:2; :: thesis: verum

end;

suppose k in Seg m ; :: thesis: ( 0 <= k & k <= m )

then ( 0 + 1 <= k & k <= m ) by FINSEQ_1:3;
hence ( 0 <= k & k <= m ) by NAT_1:13; :: thesis: verum

end;

end;

end;

then ( 0 + 1 <= k + 1 & k + 1 <= m + 1 ) by XREAL_1:8;
hence k + 1 in Seg (len F₃(x)) by A8, FINSEQ_1:3; :: thesis: verum

end;

hence ( k in H₁(x) implies k + 1 in Seg (len F₃(x)) ) ; :: thesis: ( k + 1 in Seg (len F₃(x)) implies k in H₁(x) )
assume A9: k + 1 in Seg (len F₃(x)) ; :: thesis: k in H₁(x)
then consider m being Element of NAT such that
A10: ( m + 1 = len F₃(x) & F . x = {0 } \/ (Seg m) ) by A4, A6, FINSEQ_1:4;
k in {0 } \/ (Seg m)

proof

per cases ( k = 0 or k <> 0 ) ;

suppose k = 0 ; :: thesis: k in {0 } \/ (Seg m)

then k in {0 } by TARSKI:def 1;
hence k in {0 } \/ (Seg m) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: k in {0 } \/ (Seg m)

then 0 < k by NAT_1:3;
then A11: 0 + 1 <= k by NAT_1:13;
( 1 <= k + 1 & k + 1 <= len F₃(x) ) by A9, FINSEQ_1:3;
then ( 1 <= k & k <= m ) by A10, A11, XREAL_1:8;
then k in Seg m by FINSEQ_1:3;
hence k in {0 } \/ (Seg m) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence k in H₁(x) by A10; :: thesis: verum

end;

A12: for T being finite-branching DecoratedTree
for x being set
for t being Element of dom T st x in F₁() holds
{ (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) }

proof

let T be finite-branching DecoratedTree; :: thesis: for x being set
for t being Element of dom T st x in F₁() holds
{ (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) }
let x be set ; :: thesis: for t being Element of dom T st x in F₁() holds
{ (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) }
let t be Element of dom T; :: thesis: ( x in F₁() implies { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) } )
assume A13: x in F₁() ; :: thesis: { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } = { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) }
thus { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } c= { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) } :: according to XBOOLE_0:def 10 :: thesis: { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) } c= { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } or y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) } )
assume y in { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } ; :: thesis: y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) }
then consider k being Element of NAT such that
A14: ( y = t ^ <*k*> & k in H₁(x) ) ;
( y = t ^ <*k*> & k + 1 in Seg (len F₃(x)) ) by A5, A13, A14;
hence y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) } ; :: thesis: verum

end;

thus { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) } c= { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) } or y in { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } )
assume y in { (t ^ <*m*>) where m is Element of NAT : m + 1 in Seg (len F₃(x)) } ; :: thesis: y in { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) }
then consider m being Element of NAT such that
A15: ( y = t ^ <*m*> & m + 1 in Seg (len F₃(x)) ) ;
( y = t ^ <*m*> & m in H₁(x) ) by A5, A13, A15;
hence y in { (t ^ <*k*>) where k is Element of NAT : k in H₁(x) } ; :: thesis: verum

end;

end;

defpred S₂[ set , set ] means ex x being set ex n being Element of NAT st
( x in F₁() & $1 = [x,n] & ( ( n in H₁(x) & $2 = F₃(x) . (n + 1) ) or ( not n in H₁(x) & $2 = F₂() ) ) );
A16: for c being Element of [:F₁(),NAT :] ex y being Element of F₁() st S₂[c,y]

proof

let c be Element of [:F₁(),NAT :]; :: thesis: ex y being Element of F₁() st S₂[c,y]
( c `1 in F<sub>1</sub>() & c `2 in NAT ) by MCART_1:10;
then consider x being Element of F₁(), n being Element of NAT such that
A17: ( x = c `1 & n = c `2 ) ;
A18: c = [x,n] by A17, MCART_1:23;

per cases ( n in H₁(x) or not n in H₁(x) ) ;

suppose A19: n in H₁(x) ; :: thesis: ex y being Element of F₁() st S₂[c,y]

then n + 1 in Seg (len F₃(x)) by A5;
then n + 1 in dom F₃(x) by FINSEQ_1:def 3;
then A20: F₃(x) . (n + 1) in rng F₃(x) by FUNCT_1:def 5;
rng F₃(x) c= F₁() by FINSEQ_1:def 4;
then consider y being Element of F₁() such that
A21: y = F₃(x) . (n + 1) by A20;
thus ex y being Element of F₁() st S₂[c,y] by A18, A19, A21; :: thesis: verum

end;

suppose not n in H₁(x) ; :: thesis: ex y being Element of F₁() st S₂[c,y]

hence ex y being Element of F₁() st S₂[c,y] by A18; :: thesis: verum

end;

end;

end;

ex S being Function of [:F₁(),NAT :],F₁() st
for c being Element of [:F₁(),NAT :] holds S₂[c,S . c] from FUNCT_2:sch 3(A16);
then consider S being Function of [:F₁(),NAT :],F₁() such that
A22: for c being Element of [:F₁(),NAT :] holds S₂[c,S . c] ;
A23: for n being Element of NAT
for x being set st x in F₁() & n in H₁(x) holds
S . x,n = F₃(x) . (n + 1)

proof

let n be Element of NAT ; :: thesis: for x being set st x in F₁() & n in H₁(x) holds
S . x,n = F₃(x) . (n + 1)
let x be set ; :: thesis: ( x in F₁() & n in H₁(x) implies S . x,n = F₃(x) . (n + 1) )
assume A24: ( x in F₁() & n in H₁(x) ) ; :: thesis: S . x,n = F₃(x) . (n + 1)
A25: [x,n] `1 = x by MCART_1:def 1;
[x,n] `2 = n by MCART_1:def 2;
then [x,n] in [:F₁(),NAT :] by A24, A25, MCART_1:11;
then consider c being Element of [:F₁(),NAT :] such that
A26: c = [x,n] ;
consider x' being set , n' being Element of NAT such that
A27: ( x' in F₁() & c = [x',n'] & ( ( n' in H₁(x') & S . c = F₃(x') . (n' + 1) ) or ( not n' in H₁(x') & S . c = F₂() ) ) ) by A22;
( x' = x & n' = n ) by A26, A27, ZFMISC_1:33;
hence S . x,n = F₃(x) . (n + 1) by A24, A27; :: thesis: verum

end;

A28: for n being Element of NAT
for x being set
for m being Element of NAT st m + 1 = len F₃(x) & x in F₁() holds
( n in H₁(x) iff ( 0 <= n & n <= m ) )

proof

let n be Element of NAT ; :: thesis: for x being set
for m being Element of NAT st m + 1 = len F₃(x) & x in F₁() holds
( n in H₁(x) iff ( 0 <= n & n <= m ) )
let x be set ; :: thesis: for m being Element of NAT st m + 1 = len F₃(x) & x in F₁() holds
( n in H₁(x) iff ( 0 <= n & n <= m ) )
let m be Element of NAT ; :: thesis: ( m + 1 = len F₃(x) & x in F₁() implies ( n in H₁(x) iff ( 0 <= n & n <= m ) ) )
assume A29: ( m + 1 = len F₃(x) & x in F₁() ) ; :: thesis: ( n in H₁(x) iff ( 0 <= n & n <= m ) )
thus ( n in H₁(x) implies ( 0 <= n & n <= m ) ) :: thesis: ( 0 <= n & n <= m implies n in H₁(x) )

proof

assume A30: n in H₁(x) ; :: thesis: ( 0 <= n & n <= m )
consider k being Element of NAT such that
A31: ( k + 1 = len F₃(x) & H₁(x) = {0 } \/ (Seg k) ) by A4, A29;

per cases ( n in {0 } or n in Seg m ) by A29, A30, A31, XBOOLE_0:def 3;

suppose n in {0 } ; :: thesis: ( 0 <= n & n <= m )

then n = 0 by TARSKI:def 1;
hence ( 0 <= n & n <= m ) by NAT_1:2; :: thesis: verum

end;

suppose n in Seg m ; :: thesis: ( 0 <= n & n <= m )

then ( 1 <= n & n <= m ) by FINSEQ_1:3;
hence ( 0 <= n & n <= m ) by XXREAL_0:2; :: thesis: verum

end;

end;

end;

thus ( 0 <= n & n <= m implies n in H₁(x) ) :: thesis: verum

proof

assume A32: ( 0 <= n & n <= m ) ; :: thesis: n in H₁(x)
consider k being Element of NAT such that
A33: ( k + 1 = len F₃(x) & H₁(x) = {0 } \/ (Seg k) ) by A4, A29;

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: n in H₁(x)

then n in {0 } by TARSKI:def 1;
hence n in H₁(x) by A33, XBOOLE_0:def 3; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: n in H₁(x)

then 0 < n by NAT_1:3;
then 0 + 1 <= n by NAT_1:13;
then n in Seg m by A32, FINSEQ_1:3;
hence n in H₁(x) by A29, A33, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

A34: for d being Element of F₁()
for k1, k2 being Element of NAT st k1 <= k2 & k2 in H₁(d) holds
k1 in H₁(d)

proof

let d be Element of F₁(); :: thesis: for k1, k2 being Element of NAT st k1 <= k2 & k2 in H₁(d) holds
k1 in H₁(d)
let k1, k2 be Element of NAT ; :: thesis: ( k1 <= k2 & k2 in H₁(d) implies k1 in H₁(d) )
assume A35: ( k1 <= k2 & k2 in H₁(d) ) ; :: thesis: k1 in H₁(d)
then ( len F₃(d) <> 0 & ex m being Element of NAT st
( m + 1 = len F₃(d) & F . d = {0 } \/ (Seg m) ) ) by A4;
then consider m being Element of NAT such that
A36: m + 1 = len F₃(d) ;
( 0 <= k2 & k2 <= m ) by A28, A35, A36;
then ( 0 <= k1 & k1 <= m ) by A35, NAT_1:2, XXREAL_0:2;
hence k1 in H₁(d) by A28, A36; :: thesis: verum

end;

consider T being DecoratedTree of such that
A37: ( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Element of NAT : k in H₁(T . t) } & ( for n being Element of NAT st n in H₁(T . t) holds
T . (t ^ <*n*>) = S . (T . t),n ) ) ) ) from TREES_2:sch 8(A34);
T is finite-branching

proof

for t being Element of dom T holds succ t is finite

proof

let t be Element of dom T; :: thesis: succ t is finite
A38: succ t = { (t ^ <*k*>) where k is Element of NAT : k in H₁(T . t) } by A37;
defpred S₃[ set , set ] means ex m being Element of NAT st
( m + 1 = $1 & $2 = t ^ <*m*> );
A40: for k being Nat st k in Seg (len F₃((T . t))) holds
ex x being set st S₃[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F₃((T . t))) implies ex x being set st S₃[k,x] )
assume k in Seg (len F₃((T . t))) ; :: thesis: ex x being set st S₃[k,x]
then k <> 0 by FINSEQ_1:3;
then consider m being Nat such that
A41: m + 1 = k by NAT_1:6;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
consider x being set such that
A42: x = t ^ <*m*> ;
thus ex x being set st S₃[k,x] by A41, A42; :: thesis: verum

end;

ex L being FinSequence st
( dom L = Seg (len F₃((T . t))) & ( for k being Nat st k in Seg (len F₃((T . t))) holds
S₃[k,L . k] ) ) from FINSEQ_1:sch 1(A40);
then consider L being FinSequence such that
A43: ( dom L = Seg (len F₃((T . t))) & ( for k being Nat st k in Seg (len F₃((T . t))) holds
S₃[k,L . k] ) ) ;
A44: for k being Element of NAT st 1 <= k + 1 & k + 1 <= len F₃((T . t)) holds
L . (k + 1) = t ^ <*k*>

proof

let k be Element of NAT ; :: thesis: ( 1 <= k + 1 & k + 1 <= len F₃((T . t)) implies L . (k + 1) = t ^ <*k*> )
assume ( 1 <= k + 1 & k + 1 <= len F₃((T . t)) ) ; :: thesis: L . (k + 1) = t ^ <*k*>
then k + 1 in Seg (len F₃((T . t))) by FINSEQ_1:3;
then consider m being Element of NAT such that
A45: ( m + 1 = k + 1 & L . (k + 1) = t ^ <*m*> ) by A43;
thus L . (k + 1) = t ^ <*k*> by A45; :: thesis: verum

end;

succ t = rng L

proof

thus succ t c= rng L :: according to XBOOLE_0:def 10 :: thesis: rng L c= succ t

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in succ t or x in rng L )
assume x in succ t ; :: thesis: x in rng L
then consider k being Element of NAT such that
A46: ( x = t ^ <*k*> & k in H₁(T . t) ) by A38;
A47: k + 1 in Seg (len F₃((T . t))) by A5, A46;
then ( 1 <= k + 1 & k + 1 <= len F₃((T . t)) ) by FINSEQ_1:3;
then L . (k + 1) = t ^ <*k*> by A44;
hence x in rng L by A43, A46, A47, FUNCT_1:def 5; :: thesis: verum

end;

thus rng L c= succ t :: thesis: verum

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng L or y in succ t )
assume y in rng L ; :: thesis: y in succ t
then consider m being set such that
A48: ( m in dom L & y = L . m ) by FUNCT_1:def 5;
reconsider m = m as Element of NAT by A48;
A49: ( 1 <= m & m <= len F₃((T . t)) ) by A43, A48, FINSEQ_1:3;
m <> 0 by A43, A48, FINSEQ_1:3;
then consider k being Nat such that
A50: k + 1 = m by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
( y = t ^ <*k*> & k in H₁(T . t) ) by A5, A43, A44, A48, A49, A50;
hence y in succ t by A38; :: thesis: verum

end;

end;

hence succ t is finite ; :: thesis: verum

end;

then dom T is finite-branching by TREES_9:def 2;
hence T is finite-branching by TREES_9:def 4; :: thesis: verum

end;

then reconsider T = T as finite-branching DecoratedTree of ;

now

let t be Element of dom T; :: thesis: for w being Element of F₁() st w = T . t holds
succ T,t = F₃(w)
let w be Element of F₁(); :: thesis: ( w = T . t implies succ T,t = F₃(w) )
assume A51: w = T . t ; :: thesis: succ T,t = F₃(w)
A52: dom (succ T,t) = dom F₃(w)

proof

A53: dom F₃(w) = Seg (len F₃(w)) by FINSEQ_1:def 3;
A54: dom (t succ ) = Seg (len (t succ )) by FINSEQ_1:def 3;
succ t = { (t ^ <*k*>) where k is Element of NAT : k in H₁(w) } by A37, A51;
then A55: succ t = { (t ^ <*k*>) where k is Element of NAT : k + 1 in Seg (len F₃(w)) } by A12;
dom F₃(w) = dom (t succ )

proof

thus dom F₃(w) c= dom (t succ ) :: according to XBOOLE_0:def 10 :: thesis: dom (t succ ) c= dom F₃(w)

proof

let n' be set ; :: according to TARSKI:def 3 :: thesis: ( not n' in dom F₃(w) or n' in dom (t succ ) )
assume A56: n' in dom F₃(w) ; :: thesis: n' in dom (t succ )
A57: Seg (len F₃(w)) = { k where k is Element of NAT : ( 1 <= k & k <= len F₃(w) ) } by FINSEQ_1:def 1;
then consider m being Element of NAT such that
A58: ( n' = m & 1 <= m & m <= len F₃(w) ) by A53, A56;
0 <> m by A58;
then consider n being Nat such that
A59: m = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
n + 1 in Seg (len F₃(w)) by A57, A58, A59;
then t ^ <*n*> in succ t by A55;
hence n' in dom (t succ ) by A58, A59, Th12; :: thesis: verum

end;

thus dom (t succ ) c= dom F₃(w) :: thesis: verum

proof

let n' be set ; :: according to TARSKI:def 3 :: thesis: ( not n' in dom (t succ ) or n' in dom F₃(w) )
assume A60: n' in dom (t succ ) ; :: thesis: n' in dom F₃(w)
A61: Seg (len (t succ )) = { k where k is Element of NAT : ( 1 <= k & k <= len (t succ ) ) } by FINSEQ_1:def 1;
then consider m being Element of NAT such that
A62: ( n' = m & 1 <= m & m <= len (t succ ) ) by A54, A60;
0 <> m by A62;
then consider n being Nat such that
A63: m = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
n + 1 in dom (t succ ) by A54, A61, A62, A63;
then t ^ <*n*> in dom T by Th12;
then t ^ <*n*> in succ t ;
then consider k being Element of NAT such that
A64: ( t ^ <*k*> = t ^ <*n*> & k + 1 in Seg (len F₃(w)) ) by A55;
<*k*> = <*n*> by A64, FINSEQ_1:46;
hence n' in dom F₃(w) by A53, A62, A63, A64, TREES_1:23; :: thesis: verum

end;

end;

hence dom (succ T,t) = dom F₃(w) by Th11; :: thesis: verum

end;

for m being Nat st m in dom (succ T,t) holds
(succ T,t) . m = F₃(w) . m

proof

let m be Nat; :: thesis: ( m in dom (succ T,t) implies (succ T,t) . m = F₃(w) . m )
assume A65: m in dom (succ T,t) ; :: thesis: (succ T,t) . m = F₃(w) . m
then A66: m in Seg (len F₃(w)) by A52, FINSEQ_1:def 3;
Seg (len F₃(w)) = { k where k is Element of NAT : ( 1 <= k & k <= len F₃(w) ) } by FINSEQ_1:def 1;
then consider k being Element of NAT such that
A67: ( m = k & 1 <= k & k <= len F₃(w) ) by A66;
0 <> k by A67;
then consider n being Nat such that
A68: m = n + 1 by A67, NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
n + 1 in dom (t succ ) by A65, A68, Th11;
then A69: t ^ <*n*> in dom T by Th12;
consider l being Element of NAT such that
A70: ( l + 1 = len F₃((T . t)) & F . (T . t) = {0 } \/ (Seg l) ) by A4, A51, A66, FINSEQ_1:4;
( 0 + 1 <= n + 1 & n + 1 <= l + 1 ) by A51, A67, A68, A70;
then A71: ( 0 <= n & n <= l ) by XREAL_1:8;
A72: n in {0 } \/ (Seg l)

proof

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: n in {0 } \/ (Seg l)

then n in {0 } by TARSKI:def 1;
hence n in {0 } \/ (Seg l) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: n in {0 } \/ (Seg l)

then 0 < n by NAT_1:3;
then 0 + 1 <= n by NAT_1:13;
then n in Seg l by A71, FINSEQ_1:3;
hence n in {0 } \/ (Seg l) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

(succ T,t) . (n + 1) = T . (t ^ <*n*>) by A69, Th13
.= S . (T . t),n by A37, A70, A72
.= F₃(w) . (n + 1) by A23, A51, A70, A72 ;
hence (succ T,t) . m = F₃(w) . m by A68; :: thesis: verum

end;

hence succ T,t = F₃(w) by A52, FINSEQ_1:17; :: thesis: verum

end;

hence ex T being finite-branching DecoratedTree of st
( T . {} = F₂() & ( for t being Element of dom T
for w being Element of F₁() st w = T . t holds
succ T,t = F₃(w) ) ) by A37; :: thesis: verum