defpred S₁[ Ordinal, Sequence] means ( dom $2 = $1 & ( 0 in $1 implies $2 . 0 = F₂() ) & ( for A1 being Ordinal st succ A1 in $1 holds
$2 . (succ A1) = F₃(A1,($2 . A1)) ) & ( for A1 being Ordinal st A1 in $1 & A1 <> 0 & A1 is limit_ordinal holds
$2 . A1 = F₄(A1,($2 | A1)) ) );
defpred S₂[ Ordinal] means ex L being Sequence st S₁[$1,L];
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S₂[C] ) holds
S₂[B]

proof

defpred S₃[ object , object ] means ( $1 is Ordinal & $2 is Sequence & ( for A being Ordinal
for L being Sequence st A = $1 & L = $2 holds
S₁[A,L] ) );
let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S₂[C] ) implies S₂[B] )
assume A2: for C being Ordinal st C in B holds
ex L being Sequence st S₁[C,L] ; :: thesis: S₂[B]
A3: for a, b, c being object st S₃[a,b] & S₃[a,c] holds
b = c

proof

let a, b, c be object ; :: thesis: ( S₃[a,b] & S₃[a,c] implies b = c )
assume that
A4: a is Ordinal and
A5: b is Sequence and
A6: for A being Ordinal
for L being Sequence st A = a & L = b holds
S₁[A,L] and
a is Ordinal and
A7: c is Sequence and
A8: for A being Ordinal
for L being Sequence st A = a & L = c holds
S₁[A,L] ; :: thesis: b = c
reconsider a = a as Ordinal by A4;
reconsider c = c as Sequence by A7;
A9: dom c = a by A8;
A10: for A being Ordinal st A in a & A <> 0 & A is limit_ordinal holds
c . A = F₄(A,(c | A)) by A8;
A11: for A being Ordinal st succ A in a holds
c . (succ A) = F₃(A,(c . A)) by A8;
A12: ( 0 in a implies c . 0 = F₂() ) by A8;
reconsider b = b as Sequence by A5;
A13: ( 0 in a implies b . 0 = F₂() ) by A6;
A14: for A being Ordinal st succ A in a holds
b . (succ A) = F₃(A,(b . A)) by A6;
A15: for A being Ordinal st A in a & A <> 0 & A is limit_ordinal holds
b . A = F₄(A,(b | A)) by A6;
A16: dom b = a by A6;
b = c from ORDINAL2:sch 4(A16, A13, A14, A15, A9, A12, A11, A10);
hence b = c ; :: thesis: verum

end;

consider G being Function such that
A17: for a, b being object holds
( [a,b] in G iff ( a in B & S₃[a,b] ) ) from FUNCT_1:sch 1(A3);
defpred S₄[ object , object ] means ex A being Ordinal ex L being Sequence st
( A = $1 & L = G . $1 & ( ( A = 0 & $2 = F₂() ) or ex B being Ordinal st
( A = succ B & $2 = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & $2 = F₄(A,L) ) ) );
A18: dom G = B

proof

thus for a being object st a in dom G holds
a in B :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: B c= dom G

proof

let a be object ; :: thesis: ( a in dom G implies a in B )
assume a in dom G ; :: thesis: a in B
then ex b being object st [a,b] in G by XTUPLE_0:def 12;
hence a in B by A17; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in dom G )
assume A19: a in B ; :: thesis: a in dom G
then reconsider a9 = a as Ordinal ;
consider L being Sequence such that
A20: S₁[a9,L] by A2, A19;
for A being Ordinal
for K being Sequence st A = a9 & K = L holds
S₁[A,K] by A20;
then [a9,L] in G by A17, A19;
hence a in dom G by XTUPLE_0:def 12; :: thesis: verum

end;

A21: for a being object st a in B holds
ex b being object st S₄[a,b]

proof

let a be object ; :: thesis: ( a in B implies ex b being object st S₄[a,b] )
assume A22: a in B ; :: thesis: ex b being object st S₄[a,b]
then reconsider A = a as Ordinal ;
consider c being object such that
A23: [a,c] in G by A18, A22, XTUPLE_0:def 12;
reconsider L = c as Sequence by A17, A23;

A24: now :: thesis: ( ex C being Ordinal st A = succ C implies ex b being object st S₄[a,b] )

given C being Ordinal such that A25: A = succ C ; :: thesis: ex b being object st S₄[a,b]
thus ex b being object st S₄[a,b] :: thesis: verum

proof

take F₃(C,(L . C)) ; :: thesis: S₄[a,F₃(C,(L . C))]
take A ; :: thesis: ex L being Sequence st
( A = a & L = G . a & ( ( A = 0 & F₃(C,(L . C)) = F₂() ) or ex B being Ordinal st
( A = succ B & F₃(C,(L . C)) = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₃(C,(L . C)) = F₄(A,L) ) ) )
take L ; :: thesis: ( A = a & L = G . a & ( ( A = 0 & F₃(C,(L . C)) = F₂() ) or ex B being Ordinal st
( A = succ B & F₃(C,(L . C)) = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₃(C,(L . C)) = F₄(A,L) ) ) )
thus ( A = a & L = G . a ) by A23, FUNCT_1:1; :: thesis: ( ( A = 0 & F₃(C,(L . C)) = F₂() ) or ex B being Ordinal st
( A = succ B & F₃(C,(L . C)) = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₃(C,(L . C)) = F₄(A,L) ) )
thus ( ( A = 0 & F₃(C,(L . C)) = F₂() ) or ex B being Ordinal st
( A = succ B & F₃(C,(L . C)) = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₃(C,(L . C)) = F₄(A,L) ) ) by A25; :: thesis: verum

end;

end;

A26: now :: thesis: ( A <> 0 & ( for C being Ordinal holds A <> succ C ) implies S₄[a,F₄(A,L)] )

assume A27: ( A <> 0 & ( for C being Ordinal holds A <> succ C ) ) ; :: thesis: S₄[a,F₄(A,L)]
thus S₄[a,F₄(A,L)] :: thesis: verum

proof

take A ; :: thesis: ex L being Sequence st
( A = a & L = G . a & ( ( A = 0 & F₄(A,L) = F₂() ) or ex B being Ordinal st
( A = succ B & F₄(A,L) = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₄(A,L) = F₄(A,L) ) ) )
take L ; :: thesis: ( A = a & L = G . a & ( ( A = 0 & F₄(A,L) = F₂() ) or ex B being Ordinal st
( A = succ B & F₄(A,L) = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₄(A,L) = F₄(A,L) ) ) )
thus ( A = a & L = G . a ) by A23, FUNCT_1:1; :: thesis: ( ( A = 0 & F₄(A,L) = F₂() ) or ex B being Ordinal st
( A = succ B & F₄(A,L) = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₄(A,L) = F₄(A,L) ) )
thus ( ( A = 0 & F₄(A,L) = F₂() ) or ex B being Ordinal st
( A = succ B & F₄(A,L) = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₄(A,L) = F₄(A,L) ) ) by A27, ORDINAL1:29; :: thesis: verum

end;

end;

now :: thesis: ( A = 0 implies S₄[a,F₂()] )

assume A28: A = 0 ; :: thesis: S₄[a,F₂()]
thus S₄[a,F₂()] :: thesis: verum

proof

take A ; :: thesis: ex L being Sequence st
( A = a & L = G . a & ( ( A = 0 & F₂() = F₂() ) or ex B being Ordinal st
( A = succ B & F₂() = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₂() = F₄(A,L) ) ) )
take L ; :: thesis: ( A = a & L = G . a & ( ( A = 0 & F₂() = F₂() ) or ex B being Ordinal st
( A = succ B & F₂() = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₂() = F₄(A,L) ) ) )
thus ( A = a & L = G . a ) by A23, FUNCT_1:1; :: thesis: ( ( A = 0 & F₂() = F₂() ) or ex B being Ordinal st
( A = succ B & F₂() = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₂() = F₄(A,L) ) )
thus ( ( A = 0 & F₂() = F₂() ) or ex B being Ordinal st
( A = succ B & F₂() = F₃(B,(L . B)) ) or ( A <> 0 & A is limit_ordinal & F₂() = F₄(A,L) ) ) by A28; :: thesis: verum

end;

end;

hence ex b being object st S₄[a,b] by A24, A26; :: thesis: verum

end;

A29: for a, b, c being object st a in B & S₄[a,b] & S₄[a,c] holds
b = c

proof

let a, b, c be object ; :: thesis: ( a in B & S₄[a,b] & S₄[a,c] implies b = c )
assume a in B ; :: thesis: ( not S₄[a,b] or not S₄[a,c] or b = c )
given Ab being Ordinal, Lb being Sequence such that A30: Ab = a and
A31: Lb = G . a and
A32: ( ( Ab = 0 & b = F₂() ) or ex B being Ordinal st
( Ab = succ B & b = F₃(B,(Lb . B)) ) or ( Ab <> 0 & Ab is limit_ordinal & b = F₄(Ab,Lb) ) ) ; :: thesis: ( not S₄[a,c] or b = c )
given Ac being Ordinal, Lc being Sequence such that A33: Ac = a and
A34: Lc = G . a and
A35: ( ( Ac = 0 & c = F₂() ) or ex B being Ordinal st
( Ac = succ B & c = F₃(B,(Lc . B)) ) or ( Ac <> 0 & Ac is limit_ordinal & c = F₄(Ac,Lc) ) ) ; :: thesis: b = c

now :: thesis: ( ex C being Ordinal st Ab = succ C implies b = c )

given C being Ordinal such that A36: Ab = succ C ; :: thesis: b = c
consider A being Ordinal such that
A37: Ab = succ A and
A38: b = F₃(A,(Lb . A)) by A32, A36, ORDINAL1:29;
consider D being Ordinal such that
A39: Ac = succ D and
A40: c = F₃(D,(Lc . D)) by A30, A33, A35, A36, ORDINAL1:29;
A = D by A30, A33, A37, A39, ORDINAL1:7;
hence b = c by A31, A34, A38, A40; :: thesis: verum

end;

hence b = c by A30, A31, A32, A33, A34, A35; :: thesis: verum

end;

consider F being Function such that
A41: ( dom F = B & ( for a being object st a in B holds
S₄[a,F . a] ) ) from FUNCT_1:sch 2(A29, A21);
reconsider L = F as Sequence by A41, ORDINAL1:def 7;
take L ; :: thesis: S₁[B,L]
thus dom L = B by A41; :: thesis: ( ( 0 in B implies L . 0 = F₂() ) & ( for A1 being Ordinal st succ A1 in B holds
L . (succ A1) = F₃(A1,(L . A1)) ) & ( for A1 being Ordinal st A1 in B & A1 <> 0 & A1 is limit_ordinal holds
L . A1 = F₄(A1,(L | A1)) ) )
thus ( 0 in B implies L . 0 = F₂() ) :: thesis: ( ( for A1 being Ordinal st succ A1 in B holds
L . (succ A1) = F₃(A1,(L . A1)) ) & ( for A1 being Ordinal st A1 in B & A1 <> 0 & A1 is limit_ordinal holds
L . A1 = F₄(A1,(L | A1)) ) )

proof

assume 0 in B ; :: thesis: L . 0 = F₂()
then ex A being Ordinal ex K being Sequence st
( A = 0 & K = G . 0 & ( ( A = 0 & F . 0 = F₂() ) or ex B being Ordinal st
( A = succ B & F . 0 = F₃(B,(K . B)) ) or ( A <> 0 & A is limit_ordinal & F . 0 = F₄(A,K) ) ) ) by A41;
hence L . 0 = F₂() ; :: thesis: verum

end;

A42: for A being Ordinal
for L1 being Sequence st A in B & L1 = G . A holds
L | A = L1

proof

defpred S₅[ Ordinal] means for L1 being Sequence st $1 in B & L1 = G . $1 holds
L | $1 = L1;
A43: for A being Ordinal st ( for C being Ordinal st C in A holds
S₅[C] ) holds
S₅[A]

proof

let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S₅[C] ) implies S₅[A] )
assume for C being Ordinal st C in A holds
for L1 being Sequence st C in B & L1 = G . C holds
L | C = L1 ; :: thesis: S₅[A]
let L1 be Sequence; :: thesis: ( A in B & L1 = G . A implies L | A = L1 )
assume that
A44: A in B and
A45: L1 = G . A ; :: thesis: L | A = L1
A46: [A,L1] in G by A18, A44, A45, FUNCT_1:1;
then A47: S₁[A,L1] by A17;

A48: now :: thesis: for x being object st x in A holds
L1 . x = (L | A) . x

let x be object ; :: thesis: ( x in A implies L1 . x = (L | A) . x )
assume A49: x in A ; :: thesis: L1 . x = (L | A) . x
then reconsider x9 = x as Ordinal ;
A50: x9 in B by A44, A49, ORDINAL1:10;
then consider A1 being Ordinal, L2 being Sequence such that
A51: A1 = x9 and
A52: L2 = G . x9 and
A53: ( ( A1 = 0 & L . x9 = F₂() ) or ex B being Ordinal st
( A1 = succ B & L . x9 = F₃(B,(L2 . B)) ) or ( A1 <> 0 & A1 is limit_ordinal & L . x9 = F₄(A1,L2) ) ) by A41;
for D being Ordinal
for L3 being Sequence st D = x9 & L3 = L1 | x9 holds
S₁[D,L3]

proof

let D be Ordinal; :: thesis: for L3 being Sequence st D = x9 & L3 = L1 | x9 holds
S₁[D,L3]
let L3 be Sequence; :: thesis: ( D = x9 & L3 = L1 | x9 implies S₁[D,L3] )
assume that
A54: D = x9 and
A55: L3 = L1 | x9 ; :: thesis: S₁[D,L3]
x9 c= A by A49, ORDINAL1:def 2;
hence dom L3 = D by A47, A54, A55, RELAT_1:62; :: thesis: ( ( 0 in D implies L3 . 0 = F₂() ) & ( for A1 being Ordinal st succ A1 in D holds
L3 . (succ A1) = F₃(A1,(L3 . A1)) ) & ( for A1 being Ordinal st A1 in D & A1 <> 0 & A1 is limit_ordinal holds
L3 . A1 = F₄(A1,(L3 | A1)) ) )
thus ( 0 in D implies L3 . 0 = F₂() ) by A47, A49, A54, A55, FUNCT_1:49, ORDINAL1:10; :: thesis: ( ( for A1 being Ordinal st succ A1 in D holds
L3 . (succ A1) = F₃(A1,(L3 . A1)) ) & ( for A1 being Ordinal st A1 in D & A1 <> 0 & A1 is limit_ordinal holds
L3 . A1 = F₄(A1,(L3 | A1)) ) )
thus for C being Ordinal st succ C in D holds
L3 . (succ C) = F₃(C,(L3 . C)) :: thesis: for A1 being Ordinal st A1 in D & A1 <> 0 & A1 is limit_ordinal holds
L3 . A1 = F₄(A1,(L3 | A1))

proof

let C be Ordinal; :: thesis: ( succ C in D implies L3 . (succ C) = F₃(C,(L3 . C)) )
assume A56: succ C in D ; :: thesis: L3 . (succ C) = F₃(C,(L3 . C))
C in succ C by ORDINAL1:6;
then A57: (L1 | x9) . C = L1 . C by A54, A56, FUNCT_1:49, ORDINAL1:10;
( succ C in A & (L1 | x9) . (succ C) = L1 . (succ C) ) by A49, A54, A56, FUNCT_1:49, ORDINAL1:10;
hence L3 . (succ C) = F₃(C,(L3 . C)) by A17, A46, A55, A57; :: thesis: verum

end;

let C be Ordinal; :: thesis: ( C in D & C <> 0 & C is limit_ordinal implies L3 . C = F₄(C,(L3 | C)) )
assume that
A58: C in D and
A59: ( C <> 0 & C is limit_ordinal ) ; :: thesis: L3 . C = F₄(C,(L3 | C))
C c= x9 by A54, A58, ORDINAL1:def 2;
then A60: L1 | C = L3 | C by A55, FUNCT_1:51;
C in A by A49, A54, A58, ORDINAL1:10;
then L1 . C = F₄(C,(L3 | C)) by A17, A46, A59, A60;
hence L3 . C = F₄(C,(L3 | C)) by A54, A55, A58, FUNCT_1:49; :: thesis: verum

end;

then [x9,(L1 | x9)] in G by A17, A50;
then A61: L1 | x9 = L2 by A52, FUNCT_1:1;
A62: (L | A) . x = L . x by A49, FUNCT_1:49;

now :: thesis: ( ex D being Ordinal st x9 = succ D implies L1 . x = (L | A) . x )

given D being Ordinal such that A63: x9 = succ D ; :: thesis: L1 . x = (L | A) . x
A64: L1 . x = F₃(D,(L1 . D)) by A17, A46, A49, A63;
consider C being Ordinal such that
A65: A1 = succ C and
A66: L . x9 = F₃(C,(L2 . C)) by A51, A53, A63, ORDINAL1:29;
C = D by A51, A63, A65, ORDINAL1:7;
hence L1 . x = (L | A) . x by A62, A61, A63, A66, A64, FUNCT_1:49, ORDINAL1:6; :: thesis: verum

end;

hence L1 . x = (L | A) . x by A17, A46, A49, A51, A53, A62, A61; :: thesis: verum

end;

A c= dom L by A41, A44, ORDINAL1:def 2;
then dom (L | A) = A by RELAT_1:62;
hence L | A = L1 by A47, A48, FUNCT_1:2; :: thesis: verum

end;

thus for A being Ordinal holds S₅[A] from ORDINAL1:sch 2(A43); :: thesis: verum

end;

thus for A being Ordinal st succ A in B holds
L . (succ A) = F₃(A,(L . A)) :: thesis: for A1 being Ordinal st A1 in B & A1 <> 0 & A1 is limit_ordinal holds
L . A1 = F₄(A1,(L | A1))

proof

let A be Ordinal; :: thesis: ( succ A in B implies L . (succ A) = F₃(A,(L . A)) )
assume A67: succ A in B ; :: thesis: L . (succ A) = F₃(A,(L . A))
then consider C being Ordinal, K being Sequence such that
A68: C = succ A and
A69: K = G . (succ A) and
A70: ( ( C = 0 & F . (succ A) = F₂() ) or ex B being Ordinal st
( C = succ B & F . (succ A) = F₃(B,(K . B)) ) or ( C <> 0 & C is limit_ordinal & F . (succ A) = F₄(C,K) ) ) by A41;
A71: K = L | (succ A) by A42, A67, A69;
consider D being Ordinal such that
A72: C = succ D and
A73: F . (succ A) = F₃(D,(K . D)) by A68, A70, ORDINAL1:29;
A = D by A68, A72, ORDINAL1:7;
hence L . (succ A) = F₃(A,(L . A)) by A73, A71, FUNCT_1:49, ORDINAL1:6; :: thesis: verum

end;

let D be Ordinal; :: thesis: ( D in B & D <> 0 & D is limit_ordinal implies L . D = F₄(D,(L | D)) )
assume that
A74: D in B and
A75: ( D <> 0 & D is limit_ordinal ) ; :: thesis: L . D = F₄(D,(L | D))
ex A being Ordinal ex K being Sequence st
( A = D & K = G . D & ( ( A = 0 & F . D = F₂() ) or ex B being Ordinal st
( A = succ B & F . D = F₃(B,(K . B)) ) or ( A <> 0 & A is limit_ordinal & F . D = F₄(A,K) ) ) ) by A41, A74;
hence L . D = F₄(D,(L | D)) by A42, A74, A75, ORDINAL1:29; :: thesis: verum

end;

for A being Ordinal holds S₂[A] from ORDINAL1:sch 2(A1);
hence ex L being Sequence st
( dom L = F₁() & ( 0 in F₁() implies L . 0 = F₂() ) & ( for A being Ordinal st succ A in F₁() holds
L . (succ A) = F₃(A,(L . A)) ) & ( for A being Ordinal st A in F₁() & A <> 0 & A is limit_ordinal holds
L . A = F₄(A,(L | A)) ) ) ; :: thesis: verum