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

proof

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

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

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

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

end;

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

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

end;

end;

end;

ex F being Function st
( dom F = F₁() & ( for x being object st x in F₁() holds
S₁[x,F . x] ) ) from CLASSES1:sch 1(A1);
then consider F being Function such that
A3: for x being object holds
( not x in F₁() or ( len F₃(x) = 0 & F . x = {} ) or ( len F₃(x) <> 0 & ex m being Nat st
( m + 1 = len F₃(x) & F . x = {0} \/ (Seg m) ) ) ) ;
deffunc H₁( set ) -> set = F . $1;
A4: for k being 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 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 A5: x in F₁() ; :: thesis: ( k in H₁(x) iff k + 1 in Seg (len F₃(x)) )

now :: thesis: ( k in H₁(x) implies k + 1 in Seg (len F₃(x)) )

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

proof

per cases ( k in {0} or k in Seg m ) by A6, 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 ) ; :: thesis: verum

end;

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

thus ( 0 <= k & k <= m ) by A9, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

then ( 0 + 1 <= k + 1 & k + 1 <= m + 1 ) by XREAL_1:6;
hence k + 1 in Seg (len F₃(x)) by A7, FINSEQ_1:1; :: 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 A10: k + 1 in Seg (len F₃(x)) ; :: thesis: k in H₁(x)
then len F₃(x) <> 0 ;
then consider m being Nat such that
A11: m + 1 = len F₃(x) and
A12: F . x = {0} \/ (Seg m) by A3, A5;
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 ;
then A13: 0 + 1 <= k by NAT_1:13;
k + 1 <= len F₃(x) by A10, FINSEQ_1:1;
then k <= m by A11, XREAL_1:6;
then k in Seg m by A13, FINSEQ_1:1;
hence k in {0} \/ (Seg m) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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

end;

A14: 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 Nat : k in H₁(x) } = { (t ^ <*m*>) where m is 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 Nat : k in H₁(x) } = { (t ^ <*m*>) where m is 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 Nat : k in H₁(x) } = { (t ^ <*m*>) where m is 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 Nat : k in H₁(x) } = { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) } )
assume A15: x in F₁() ; :: thesis: { (t ^ <*k*>) where k is Nat : k in H₁(x) } = { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) }
thus { (t ^ <*k*>) where k is Nat : k in H₁(x) } c= { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) } :: according to XBOOLE_0:def 10 :: thesis: { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) } c= { (t ^ <*k*>) where k is Nat : k in H₁(x) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (t ^ <*k*>) where k is Nat : k in H₁(x) } or y in { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) } )
assume y in { (t ^ <*k*>) where k is Nat : k in H₁(x) } ; :: thesis: y in { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) }
then consider k being Nat such that
A16: y = t ^ <*k*> and
A17: k in H₁(x) ;
k + 1 in Seg (len F₃(x)) by A4, A15, A17;
hence y in { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) } by A16; :: thesis: verum

end;

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) } or y in { (t ^ <*k*>) where k is Nat : k in H₁(x) } )
assume y in { (t ^ <*m*>) where m is Nat : m + 1 in Seg (len F₃(x)) } ; :: thesis: y in { (t ^ <*k*>) where k is Nat : k in H₁(x) }
then consider m being Nat such that
A18: y = t ^ <*m*> and
A19: m + 1 in Seg (len F₃(x)) ;
m in H₁(x) by A4, A15, A19;
hence y in { (t ^ <*k*>) where k is Nat : k in H₁(x) } by A18; :: thesis: verum

end;

end;

defpred S₂[ set , set ] means ex x being set ex n being 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₂() ) ) );
A20: 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 Nat such that
A21: ( x = c `1 & n = c `2 ) ;
A22: c = [x,n] by A21, MCART_1:21;

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

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

then n + 1 in Seg (len F₃(x)) by A4;
then n + 1 in dom F₃(x) by FINSEQ_1:def 3;
then A24: F₃(x) . (n + 1) in rng F₃(x) by FUNCT_1:def 3;
thus ex y being Element of F₁() st S₂[c,y] by A22, A23, A24; :: 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 A22; :: 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(A20);
then consider S being Function of [:F₁(),NAT:],F₁() such that
A25: for c being Element of [:F₁(),NAT:] holds S₂[c,S . c] ;
A26: for n being Nat
for x being set
for m being Nat st m + 1 = len F₃(x) & x in F₁() holds
( n in H₁(x) iff ( 0 <= n & n <= m ) )

proof

let n be Nat; :: thesis: for x being set
for m being 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 Nat st m + 1 = len F₃(x) & x in F₁() holds
( n in H₁(x) iff ( 0 <= n & n <= m ) )
let m be Nat; :: thesis: ( m + 1 = len F₃(x) & x in F₁() implies ( n in H₁(x) iff ( 0 <= n & n <= m ) ) )
assume that
A27: m + 1 = len F₃(x) and
A28: 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

A29: ex k being Nat st
( k + 1 = len F₃(x) & H₁(x) = {0} \/ (Seg k) ) by A3, A27, A28;
assume A30: n in H₁(x) ; :: thesis: ( 0 <= n & n <= m )

per cases ( n in {0} or n in Seg m ) by A27, A30, A29, 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 ) ; :: thesis: verum

end;

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

thus ( 0 <= n & n <= m ) by A31, FINSEQ_1:1; :: thesis: verum

end;

end;

end;

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

proof

assume that
0 <= n and
A32: n <= m ; :: thesis: n in H₁(x)
A33: ex k being Nat st
( k + 1 = len F₃(x) & H₁(x) = {0} \/ (Seg k) ) by A3, A27, A28;

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 ;
then 0 + 1 <= n by NAT_1:13;
then n in Seg m by A32, FINSEQ_1:1;
hence n in H₁(x) by A27, A33, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

A34: for d being Element of F₁()
for k1, k2 being 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 Nat st k1 <= k2 & k2 in H₁(d) holds
k1 in H₁(d)
let k1, k2 be Nat; :: thesis: ( k1 <= k2 & k2 in H₁(d) implies k1 in H₁(d) )
assume that
A35: k1 <= k2 and
A36: k2 in H₁(d) ; :: thesis: k1 in H₁(d)
ex m being Nat st
( m + 1 = len F₃(d) & F . d = {0} \/ (Seg m) ) by A3, A36;
then consider m being Nat such that
A37: m + 1 = len F₃(d) ;
k2 <= m by A26, A36, A37;
then ( 0 <= k1 & k1 <= m ) by A35, XXREAL_0:2;
hence k1 in H₁(d) by A26, A37; :: thesis: verum

end;

consider T being DecoratedTree of F₁() such that
A38: ( T . {} = F₂() & ( for t being Element of dom T holds
( succ t = { (t ^ <*k*>) where k is Nat : k in H₁(T . t) } & ( for n being Nat st n in H₁(T . t) holds
T . (t ^ <*n*>) = S . ((T . t),n) ) ) ) ) from TREES_2:sch 8(A34);
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
defpred S₃[ set , object ] means ex m being Nat st
( m + 1 = $1 & $2 = t ^ <*m*> );
A39: for k being Nat st k in Seg (len F₃((T . t))) holds
ex x being object st S₃[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len F₃((T . t))) implies ex x being object st S₃[k,x] )
assume k in Seg (len F₃((T . t))) ; :: thesis: ex x being object st S₃[k,x]
then k <> 0 by FINSEQ_1:1;
then consider m being Nat such that
A40: m + 1 = k by NAT_1:6;
reconsider m = m as Nat ;
ex x being set st x = t ^ <*m*> ;
hence ex x being object st S₃[k,x] by A40; :: 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(A39);
then consider L being FinSequence such that
A41: dom L = Seg (len F₃((T . t))) and
A42: for k being Nat st k in Seg (len F₃((T . t))) holds
S₃[k,L . k] ;
A43: for k being Nat st 1 <= k + 1 & k + 1 <= len F₃((T . t)) holds
L . (k + 1) = t ^ <*k*>

proof

let k be 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:1;
then ex m being Nat st
( m + 1 = k + 1 & L . (k + 1) = t ^ <*m*> ) by A42;
hence L . (k + 1) = t ^ <*k*> ; :: thesis: verum

end;

A44: succ t = { (t ^ <*k*>) where k is Nat : k in H₁(T . t) } by A38;
succ t c= rng L

proof

let x be object ; :: 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 Nat such that
A45: x = t ^ <*k*> and
A46: k in H₁(T . t) by A44;
A47: k + 1 in Seg (len F₃((T . t))) by A4, A46;
then ( 1 <= k + 1 & k + 1 <= len F₃((T . t)) ) by FINSEQ_1:1;
then L . (k + 1) = t ^ <*k*> by A43;
hence x in rng L by A41, A45, A47, FUNCT_1:def 3; :: thesis: verum

end;

hence succ t is finite ; :: thesis: verum

end;

then dom T is finite-branching ;
then reconsider T = T as finite-branching DecoratedTree of F₁() by Def4;
A48: for n being 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 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 that
A49: x in F₁() and
A50: n in H₁(x) ; :: thesis: S . (x,n) = F₃(x) . (n + 1)
A51: n in NAT by ORDINAL1:def 12;
[x,n] in [:F₁(),NAT:] by A49, ZFMISC_1:def 2, A51;
then consider c being Element of [:F₁(),NAT:] such that
A52: c = [x,n] ;
consider x9 being set , n9 being Nat such that
x9 in F₁() and
A53: c = [x9,n9] and
A54: ( ( n9 in H₁(x9) & S . c = F₃(x9) . (n9 + 1) ) or ( not n9 in H₁(x9) & S . c = F₂() ) ) by A25;
x9 = x by A52, A53, XTUPLE_0:1;
hence S . (x,n) = F₃(x) . (n + 1) by A50, A52, A53, A54, XTUPLE_0:1; :: thesis: verum

end;

now :: thesis: for t being Element of dom T
for w being Element of F₁() st w = T . t holds
succ (T,t) = F₃(w)

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 A55: w = T . t ; :: thesis: succ (T,t) = F₃(w)
succ t = { (t ^ <*k*>) where k is Nat : k in H₁(w) } by A38, A55;
then A56: succ t = { (t ^ <*k*>) where k is Nat : k + 1 in Seg (len F₃(w)) } by A14;
A57: dom F₃(w) = Seg (len F₃(w)) by FINSEQ_1:def 3;
A58: dom (t succ) = Seg (len (t succ)) by FINSEQ_1:def 3;
A59: dom (t succ) c= dom F₃(w)

proof

let n9 be object ; :: according to TARSKI:def 3 :: thesis: ( not n9 in dom (t succ) or n9 in dom F₃(w) )
A60: Seg (len (t succ)) = { k where k is Nat : ( 1 <= k & k <= len (t succ) ) } by FINSEQ_1:def 1;
assume n9 in dom (t succ) ; :: thesis: n9 in dom F₃(w)
then consider m being Nat such that
A61: n9 = m and
A62: 1 <= m and
A63: m <= len (t succ) by A58, A60;
0 <> m by A62;
then consider n being Nat such that
A64: m = n + 1 by NAT_1:6;
reconsider n = n as Nat ;
n + 1 in dom (t succ) by A58, A60, A62, A63, A64;
then t ^ <*n*> in dom T by Th39;
then t ^ <*n*> in succ t ;
then consider k being Nat such that
A65: t ^ <*k*> = t ^ <*n*> and
A66: k + 1 in Seg (len F₃(w)) by A56;
<*k*> = <*n*> by A65, FINSEQ_1:33;
hence n9 in dom F₃(w) by A57, A61, A64, A66, TREES_1:5; :: thesis: verum

end;

dom F₃(w) c= dom (t succ)

proof

let n9 be object ; :: according to TARSKI:def 3 :: thesis: ( not n9 in dom F₃(w) or n9 in dom (t succ) )
A67: Seg (len F₃(w)) = { k where k is Nat : ( 1 <= k & k <= len F₃(w) ) } by FINSEQ_1:def 1;
assume n9 in dom F₃(w) ; :: thesis: n9 in dom (t succ)
then consider m being Nat such that
A68: n9 = m and
A69: 1 <= m and
A70: m <= len F₃(w) by A57, A67;
0 <> m by A69;
then consider n being Nat such that
A71: m = n + 1 by NAT_1:6;
reconsider n = n as Nat ;
n + 1 in Seg (len F₃(w)) by A67, A69, A70, A71;
then t ^ <*n*> in succ t by A56;
hence n9 in dom (t succ) by A68, A71, Th39; :: thesis: verum

end;

then A72: dom F₃(w) = dom (t succ) by A59;
then A73: dom (succ (T,t)) = dom F₃(w) by Th38;
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 )
A74: Seg (len F₃(w)) = { k where k is Nat : ( 1 <= k & k <= len F₃(w) ) } by FINSEQ_1:def 1;
assume A75: m in dom (succ (T,t)) ; :: thesis: (succ (T,t)) . m = F₃(w) . m
then A76: m in Seg (len F₃(w)) by A73, FINSEQ_1:def 3;
then len F₃(w) <> 0 ;
then consider l being Nat such that
A77: l + 1 = len F₃((T . t)) and
A78: F . (T . t) = {0} \/ (Seg l) by A3, A55;
consider k being Nat such that
A79: m = k and
A80: 1 <= k and
A81: k <= len F₃(w) by A76, A74;
0 <> k by A80;
then consider n being Nat such that
A82: m = n + 1 by A79, NAT_1:6;
reconsider n = n as Nat ;
A83: n <= l by A55, A79, A81, A82, A77, XREAL_1:6;
A84: 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 ;
then 0 + 1 <= n by NAT_1:13;
then n in Seg l by A83, FINSEQ_1:1;
hence n in {0} \/ (Seg l) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

n + 1 in dom (t succ) by A75, A82, Th38;
then t ^ <*n*> in dom T by Th39;
then (succ (T,t)) . (n + 1) = T . (t ^ <*n*>) by Th40
.= S . ((T . t),n) by A38, A78, A84
.= F₃(w) . (n + 1) by A48, A55, A78, A84 ;
hence (succ (T,t)) . m = F₃(w) . m by A82; :: thesis: verum

end;

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

end;

hence ex T being finite-branching DecoratedTree of F₁() 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 A38; :: thesis: verum