:: ORDINAL2 semantic presentation

begin


scheme :: ORDINAL2:sch 1
OrdinalInd{ P1[ Ordinal] } :
 for A being Ordinal holds P1[A]
provided
A1: P1[ {} ] and
A2: for A being Ordinal st P1[A] holds
P1[ succ A] and
A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
P1[B] ) holds
P1[A]
proof
A4: for A being Ordinal st ( for B being Ordinal st B in A holds
P1[B] ) holds
P1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
P1[B] ) implies P1[A] )
assume A5: for B being Ordinal st B in A holds
P1[B] ; ::_thesis: P1[A]
A6: now__::_thesis:_(_A_<>_{}_&_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_P1[A]_)
assume that
A7: A <> {} and
A8: for B being Ordinal holds A <> succ B ; ::_thesis: P1[A]
 A is limit_ordinal by A8, ORDINAL1:29;
hence  P1[A] by A3, A5, A7; ::_thesis: verum
end;
now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_P1[A]_)
given B being Ordinal such that A9: A = succ B ; ::_thesis: P1[A]
 B in A by A9, ORDINAL1:6;
hence  P1[A] by A2, A5, A9; ::_thesis: verum
end;
hence  P1[A] by A1, A6; ::_thesis: verum
end;
thus  for A being Ordinal holds P1[A] from ORDINAL1:sch_2(A4); ::_thesis: verum
end;

theorem Th1: :: ORDINAL2:1
for A, B being Ordinal holds
( A c= B iff succ A c= succ B )
proof
let A, B be Ordinal; ::_thesis: ( A c= B iff succ A c= succ B )
 ( A c= B iff A in succ B ) by ORDINAL1:22;
hence  ( A c= B iff succ A c= succ B ) by ORDINAL1:21; ::_thesis: verum
end;

theorem Th2: :: ORDINAL2:2
for A being Ordinal holds union (succ A) = A
proof
let A be Ordinal; ::_thesis: union (succ A) = A
thus  union (succ A) c= A :: according to XBOOLE_0:def_10 ::_thesis: A c= union (succ A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (succ A) or x in A )
assume  x in union (succ A) ; ::_thesis: x in A
then consider X being set  such that
A1: x in X and
A2: X in succ A by TARSKI:def_4;
reconsider X = X as Ordinal by A2;
 X c= A by A2, ORDINAL1:22;
hence  x in A by A1; ::_thesis: verum
end;
thus  A c= union (succ A) by ORDINAL1:6, ZFMISC_1:74; ::_thesis: verum
end;

theorem :: ORDINAL2:3
for A being Ordinal holds succ A c= bool A
proof
let A be Ordinal; ::_thesis: succ A c= bool A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ A or x in bool A )
assume A1: x in succ A ; ::_thesis: x in bool A
then reconsider B = x as Ordinal ;
 ( x in A or x = A ) by A1, ORDINAL1:8;
then  B c= A by ORDINAL1:def_2;
hence  x in bool A ; ::_thesis: verum
end;

theorem :: ORDINAL2:4
{} is limit_ordinal
proof
thus  {} = union {} by ZFMISC_1:2; :: according to ORDINAL1:def_6 ::_thesis: verum
end;

theorem Th5: :: ORDINAL2:5
for A being Ordinal holds union A c= A
proof
let A be Ordinal; ::_thesis: union A c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union A or x in A )
assume  x in union A ; ::_thesis: x in A
then consider Y being set  such that
A1: x in Y and
A2: Y in A by TARSKI:def_4;
 Y c= A by A2, ORDINAL1:def_2;
hence  x in A by A1; ::_thesis: verum
end;

definition
let L be T-Sequence;
func last L ->  set  equals :: ORDINAL2:def 1
L . (union (dom L));
coherence
 L . (union (dom L)) is set ;
end;

:: deftheorem  defines last ORDINAL2:def_1_:_
 for L being T-Sequence holds last L = L . (union (dom L));

theorem :: ORDINAL2:6
for A being Ordinal
for L being T-Sequence st dom L = succ A holds
last L = L . A by Th2;

theorem :: ORDINAL2:7
for X being set holds On X c= X
proof
let X be set ; ::_thesis: On X c= X
thus  for x being set st x in On X holds
x in X by ORDINAL1:def_9; :: according to TARSKI:def_3 ::_thesis: verum
end;

theorem Th8: :: ORDINAL2:8
for A being Ordinal holds On A = A
proof
let A be Ordinal; ::_thesis: On A = A
 for x being set holds
( x in A iff ( x in A & x is Ordinal ) ) ;
hence  On A = A by ORDINAL1:def_9; ::_thesis: verum
end;

theorem Th9: :: ORDINAL2:9
for X, Y being set st X c= Y holds
On X c= On Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies On X c= On Y )
assume A1: X c= Y ; ::_thesis: On X c= On Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On X or x in On Y )
assume  x in On X ; ::_thesis: x in On Y
then  ( x in X & x is Ordinal ) by ORDINAL1:def_9;
hence  x in On Y by A1, ORDINAL1:def_9; ::_thesis: verum
end;

theorem :: ORDINAL2:10
for X being set holds Lim X c= X
proof
let X be set ; ::_thesis: Lim X c= X
thus  for x being set st x in Lim X holds
x in X by ORDINAL1:def_10; :: according to TARSKI:def_3 ::_thesis: verum
end;

theorem :: ORDINAL2:11
for X, Y being set st X c= Y holds
Lim X c= Lim Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies Lim X c= Lim Y )
assume A1: X c= Y ; ::_thesis: Lim X c= Lim Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim X or x in Lim Y )
assume  x in Lim X ; ::_thesis: x in Lim Y
then  ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) by ORDINAL1:def_10;
hence  x in Lim Y by A1, ORDINAL1:def_10; ::_thesis: verum
end;

theorem :: ORDINAL2:12
for X being set holds Lim X c= On X
proof
let X be set ; ::_thesis: Lim X c= On X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lim X or x in On X )
assume  x in Lim X ; ::_thesis: x in On X
then  ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) by ORDINAL1:def_10;
hence  x in On X by ORDINAL1:def_9; ::_thesis: verum
end;

theorem Th13: :: ORDINAL2:13
for X being set st ( for x being set st x in X holds
x is Ordinal ) holds
meet X is Ordinal
proof
let X be set ; ::_thesis: ( ( for x being set st x in X holds
x is Ordinal ) implies meet X is Ordinal )
assume A1: for x being set st x in X holds
x is Ordinal ; ::_thesis: meet X is Ordinal
now__::_thesis:_(_X_<>_{}_implies_meet_X_is_Ordinal_)
defpred S1[ Ordinal] means $1 in X;
set x = the Element of X;
assume A2: X <> {} ; ::_thesis: meet X is Ordinal
then  the Element of X is Ordinal by A1;
then A3: ex A being Ordinal st S1[A] by A2;
consider A being Ordinal such that
A4: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A3);
 for x being set holds
( x in A iff for Y being set st Y in X holds
x in Y )
proof
let x be set ; ::_thesis: ( x in A iff for Y being set st Y in X holds
x in Y )
thus  ( x in A implies for Y being set st Y in X holds
x in Y ) ::_thesis: ( ( for Y being set st Y in X holds
x in Y ) implies x in A )
proof
assume A5: x in A ; ::_thesis: for Y being set st Y in X holds
x in Y
let Y be set ; ::_thesis: ( Y in X implies x in Y )
assume A6: Y in X ; ::_thesis: x in Y
then reconsider B = Y as Ordinal by A1;
 A c= B by A4, A6;
hence  x in Y by A5; ::_thesis: verum
end;
assume  for Y being set st Y in X holds
x in Y ; ::_thesis: x in A
hence  x in A by A4; ::_thesis: verum
end;
hence  meet X is Ordinal by A2, SETFAM_1:def_1; ::_thesis: verum
end;
hence  meet X is Ordinal by SETFAM_1:def_1; ::_thesis: verum
end;

registration
cluster epsilon-transitive epsilon-connected ordinal limit_ordinal for set ;
existence
 ex b1 being Ordinal st b1 is limit_ordinal
proof
take  omega ; ::_thesis: omega is limit_ordinal
thus  omega is limit_ordinal by ORDINAL1:def_11; ::_thesis: verum
end;
end;

definition
let X be set ;
func inf X ->  Ordinal equals :: ORDINAL2:def 2
 meet (On X);
coherence
 meet (On X) is Ordinal
proof
 for x being set st x in On X holds
x is Ordinal by ORDINAL1:def_9;
hence  meet (On X) is Ordinal by Th13; ::_thesis: verum
end;
func sup X ->  Ordinal means :Def3: :: ORDINAL2:def 3
( On X c= it & ( for A being Ordinal st On X c= A holds
it c= A ) );
existence
 ex b1 being Ordinal st
( On X c= b1 & ( for A being Ordinal st On X c= A holds
b1 c= A ) )
proof
defpred S1[ Ordinal] means  On X c= $1;
 for x being set st x in On X holds
x is Ordinal by ORDINAL1:def_9;
then reconsider A = union (On X) as Ordinal by ORDINAL1:23;
 On X c= succ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On X or x in succ A )
assume A1: x in On X ; ::_thesis: x in succ A
then reconsider B = x as Ordinal by ORDINAL1:def_9;
 B c= A by A1, ZFMISC_1:74;
hence  x in succ A by ORDINAL1:22; ::_thesis: verum
end;
then A2: ex A being Ordinal st S1[A] ;
thus  ex F being Ordinal st
( S1[F] & ( for A being Ordinal st S1[A] holds
F c= A ) ) from ORDINAL1:sch_1(A2); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal st On X c= b1 & ( for A being Ordinal st On X c= A holds
b1 c= A ) & On X c= b2 & ( for A being Ordinal st On X c= A holds
b2 c= A ) holds
b1 = b2
proof
let B, C be Ordinal; ::_thesis: ( On X c= B & ( for A being Ordinal st On X c= A holds
B c= A ) & On X c= C & ( for A being Ordinal st On X c= A holds
C c= A ) implies B = C )
assume  ( On X c= B & ( for A being Ordinal st On X c= A holds
B c= A ) & On X c= C & ( for A being Ordinal st On X c= A holds
C c= A ) ) ; ::_thesis: B = C
hence  ( B c= C & C c= B ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;

:: deftheorem  defines inf ORDINAL2:def_2_:_
 for X being set holds inf X = meet (On X);

:: deftheorem Def3 defines sup ORDINAL2:def_3_:_
 for X being set
for b2 being Ordinal holds
( b2 = sup X iff ( On X c= b2 & ( for A being Ordinal st On X c= A holds
b2 c= A ) ) );

theorem :: ORDINAL2:14
for A being Ordinal
for X being set st A in X holds
inf X c= A
proof
let A be Ordinal; ::_thesis: for X being set st A in X holds
inf X c= A
let X be set ; ::_thesis: ( A in X implies inf X c= A )
assume  A in X ; ::_thesis: inf X c= A
then  A in On X by ORDINAL1:def_9;
hence  inf X c= A by SETFAM_1:3; ::_thesis: verum
end;

theorem :: ORDINAL2:15
for D being Ordinal
for X being set st On X <> {} & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X
proof
let D be Ordinal; ::_thesis: for X being set st On X <> {} & ( for A being Ordinal st A in X holds
D c= A ) holds
D c= inf X
let X be set ; ::_thesis: ( On X <> {} & ( for A being Ordinal st A in X holds
D c= A ) implies D c= inf X )
assume that
A1: On X <> {} and
A2: for A being Ordinal st A in X holds
D c= A ; ::_thesis: D c= inf X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in inf X )
assume A3: x in D ; ::_thesis: x in inf X
 for Y being set st Y in On X holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in On X implies x in Y )
assume A4: Y in On X ; ::_thesis: x in Y
then reconsider A = Y as Ordinal by ORDINAL1:def_9;
 A in X by A4, ORDINAL1:def_9;
then  D c= A by A2;
hence  x in Y by A3; ::_thesis: verum
end;
hence  x in inf X by A1, SETFAM_1:def_1; ::_thesis: verum
end;

theorem :: ORDINAL2:16
for A being Ordinal
for X, Y being set st A in X & X c= Y holds
inf Y c= inf X
proof
let A be Ordinal; ::_thesis: for X, Y being set st A in X & X c= Y holds
inf Y c= inf X
let X, Y be set ; ::_thesis: ( A in X & X c= Y implies inf Y c= inf X )
assume  A in X ; ::_thesis: ( not X c= Y or inf Y c= inf X )
then A1: On X <> {} by ORDINAL1:def_9;
assume  X c= Y ; ::_thesis: inf Y c= inf X
then  On X c= On Y by Th9;
hence  inf Y c= inf X by A1, SETFAM_1:6; ::_thesis: verum
end;

theorem :: ORDINAL2:17
for A being Ordinal
for X being set st A in X holds
inf X in X
proof
let A be Ordinal; ::_thesis: for X being set st A in X holds
inf X in X
let X be set ; ::_thesis: ( A in X implies inf X in X )
defpred S1[ Ordinal] means $1 in X;
assume  A in X ; ::_thesis: inf X in X
then A1: ex A being Ordinal st S1[A] ;
consider A being Ordinal such that
A2: ( S1[A] & ( for B being Ordinal st S1[B] holds
A c= B ) ) from ORDINAL1:sch_1(A1);
A3: A in On X by A2, ORDINAL1:def_9;
A4: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_A_implies_for_Y_being_set_st_Y_in_On_X_holds_
x_in_Y_)_&_(_(_for_Y_being_set_st_Y_in_On_X_holds_
x_in_Y_)_implies_x_in_A_)_)
let x be set ; ::_thesis: ( ( x in A implies for Y being set st Y in On X holds
x in Y ) & ( ( for Y being set st Y in On X holds
x in Y ) implies x in A ) )
thus  ( x in A implies for Y being set st Y in On X holds
x in Y ) ::_thesis: ( ( for Y being set st Y in On X holds
x in Y ) implies x in A )
proof
assume A5: x in A ; ::_thesis: for Y being set st Y in On X holds
x in Y
let Y be set ; ::_thesis: ( Y in On X implies x in Y )
assume A6: Y in On X ; ::_thesis: x in Y
then reconsider B = Y as Ordinal by ORDINAL1:def_9;
 Y in X by A6, ORDINAL1:def_9;
then  A c= B by A2;
hence  x in Y by A5; ::_thesis: verum
end;
assume  for Y being set st Y in On X holds
x in Y ; ::_thesis: x in A
hence  x in A by A3; ::_thesis: verum
end;
 On X <> {} by A2, ORDINAL1:def_9;
hence  inf X in X by A2, A4, SETFAM_1:def_1; ::_thesis: verum
end;

theorem Th18: :: ORDINAL2:18
for A being Ordinal holds sup A = A
proof
let A be Ordinal; ::_thesis: sup A = A
 ( On A = A & ( for B being Ordinal st On A c= B holds
A c= B ) ) by Th8;
hence  sup A = A by Def3; ::_thesis: verum
end;

theorem Th19: :: ORDINAL2:19
for A being Ordinal
for X being set st A in X holds
A in sup X
proof
let A be Ordinal; ::_thesis: for X being set st A in X holds
A in sup X
let X be set ; ::_thesis: ( A in X implies A in sup X )
assume  A in X ; ::_thesis: A in sup X
then A1: A in On X by ORDINAL1:def_9;
 On X c= sup X by Def3;
hence  A in sup X by A1; ::_thesis: verum
end;

theorem Th20: :: ORDINAL2:20
for D being Ordinal
for X being set st ( for A being Ordinal st A in X holds
A in D ) holds
sup X c= D
proof
let D be Ordinal; ::_thesis: for X being set st ( for A being Ordinal st A in X holds
A in D ) holds
sup X c= D
let X be set ; ::_thesis: ( ( for A being Ordinal st A in X holds
A in D ) implies sup X c= D )
assume A1: for A being Ordinal st A in X holds
A in D ; ::_thesis: sup X c= D
 On X c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On X or x in D )
assume A2: x in On X ; ::_thesis: x in D
then reconsider A = x as Ordinal by ORDINAL1:def_9;
 A in X by A2, ORDINAL1:def_9;
hence  x in D by A1; ::_thesis: verum
end;
hence  sup X c= D by Def3; ::_thesis: verum
end;

theorem :: ORDINAL2:21
for A being Ordinal
for X being set st A in sup X holds
ex B being Ordinal st
( B in X & A c= B )
proof
let A be Ordinal; ::_thesis: for X being set st A in sup X holds
ex B being Ordinal st
( B in X & A c= B )
let X be set ; ::_thesis: ( A in sup X implies ex B being Ordinal st
( B in X & A c= B ) )
assume that
A1: A in sup X and
A2: for B being Ordinal st B in X holds
not A c= B ; ::_thesis: contradiction
 for B being Ordinal st B in X holds
B in A by A2, ORDINAL1:16;
then  sup X c= A by Th20;
hence  contradiction by A1, ORDINAL1:5; ::_thesis: verum
end;

theorem :: ORDINAL2:22
for X, Y being set st X c= Y holds
sup X c= sup Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies sup X c= sup Y )
assume  X c= Y ; ::_thesis: sup X c= sup Y
then A1: On X c= On Y by Th9;
 On Y c= sup Y by Def3;
then  On X c= sup Y by A1, XBOOLE_1:1;
hence  sup X c= sup Y by Def3; ::_thesis: verum
end;

theorem :: ORDINAL2:23
for A being Ordinal holds sup {A} = succ A
proof
let A be Ordinal; ::_thesis: sup {A} = succ A
A1: On {A} c= succ A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in On {A} or x in succ A )
assume  x in On {A} ; ::_thesis: x in succ A
then  x in {A} by ORDINAL1:def_9;
then  x = A by TARSKI:def_1;
hence  x in succ A by ORDINAL1:6; ::_thesis: verum
end;
now__::_thesis:_for_B_being_Ordinal_st_On_{A}_c=_B_holds_
succ_A_c=_B
 A in {A} by TARSKI:def_1;
then A2: A in On {A} by ORDINAL1:def_9;
let B be Ordinal; ::_thesis: ( On {A} c= B implies succ A c= B )
assume  On {A} c= B ; ::_thesis: succ A c= B
hence  succ A c= B by A2, ORDINAL1:21; ::_thesis: verum
end;
hence  sup {A} = succ A by A1, Def3; ::_thesis: verum
end;

theorem :: ORDINAL2:24
for X being set holds inf X c= sup X
proof
let X be set ; ::_thesis: inf X c= sup X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in inf X or x in sup X )
set y = the Element of On X;
assume A1: x in inf X ; ::_thesis: x in sup X
then reconsider y = the Element of On X as Ordinal by ORDINAL1:def_9, SETFAM_1:1;
 On X c= sup X by Def3;
then  y in sup X by A1, SETFAM_1:1, TARSKI:def_3;
then A2: y c= sup X by ORDINAL1:def_2;
 x in y by A1, SETFAM_1:1, SETFAM_1:def_1;
hence  x in sup X by A2; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 2
TSLambda{ F1() ->  Ordinal, F2( Ordinal) ->  set } :
 ex L being T-Sequence st
( dom L = F1() & ( for A being Ordinal st A in F1() holds
L . A = F2(A) ) )
proof
deffunc H1( set ) ->  set = F2((sup (union {$1})));
consider f being Function such that
A1: ( dom f = F1() & ( for x being set st x in F1() holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
reconsider f = f as T-Sequence by A1, ORDINAL1:def_7;
take L = f; ::_thesis: ( dom L = F1() & ( for A being Ordinal st A in F1() holds
L . A = F2(A) ) )
thus  dom L = F1() by A1; ::_thesis: for A being Ordinal st A in F1() holds
L . A = F2(A)
let A be Ordinal; ::_thesis: ( A in F1() implies L . A = F2(A) )
assume  A in F1() ; ::_thesis: L . A = F2(A)
hence L . A = F2((sup (union {A}))) by A1
.= F2((sup A)) by ZFMISC_1:25
.= F2(A) by Th18 ;
::_thesis: verum
end;

definition
let f be Function;
attrf is Ordinal-yielding  means :Def4: :: ORDINAL2:def 4
 ex A being Ordinal st rng f c= A;
end;

:: deftheorem Def4 defines Ordinal-yielding ORDINAL2:def_4_:_
 for f being Function holds
( f is Ordinal-yielding iff ex A being Ordinal st rng f c= A );

registration
cluster T-Sequence-like Relation-like Function-like Ordinal-yielding for set ;
existence
 ex b1 being T-Sequence st b1 is Ordinal-yielding
proof
set A = the Ordinal;
set L = the T-Sequence of ;
take  the T-Sequence of ; ::_thesis: the T-Sequence of is Ordinal-yielding
take  the Ordinal ; :: according to ORDINAL2:def_4 ::_thesis: rng the T-Sequence of c= the Ordinal
thus  rng the T-Sequence of c= the Ordinal by RELAT_1:def_19; ::_thesis: verum
end;
end;

definition
mode Ordinal-Sequence is Ordinal-yielding T-Sequence;
end;

registration
let A be Ordinal;
cluster T-Sequence-like Relation-like A -valued Function-like  ->  Ordinal-yielding for set ;
coherence
 for b1 being T-Sequence of holds b1 is Ordinal-yielding
proof
let L be T-Sequence of ; ::_thesis: L is Ordinal-yielding
take  A ; :: according to ORDINAL2:def_4 ::_thesis: rng L c= A
thus  rng L c= A by RELAT_1:def_19; ::_thesis: verum
end;
end;

registration
let L be Ordinal-Sequence;
let A be Ordinal;
clusterL | A ->  Ordinal-yielding ;
coherence
 L | A is Ordinal-yielding
proof
consider B being Ordinal such that
A1: rng L c= B by Def4;
 L | A is Ordinal-yielding
proof
take  B ; :: according to ORDINAL2:def_4 ::_thesis: rng (L | A) c= B
 rng (L | A) c= rng L by RELAT_1:70;
hence  rng (L | A) c= B by A1, XBOOLE_1:1; ::_thesis: verum
end;
hence  L | A is Ordinal-yielding ; ::_thesis: verum
end;
end;


theorem Th25: :: ORDINAL2:25
for A being Ordinal
for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal
proof
let A be Ordinal; ::_thesis: for fi being Ordinal-Sequence st A in dom fi holds
fi . A is Ordinal
let fi be Ordinal-Sequence; ::_thesis: ( A in dom fi implies fi . A is Ordinal )
assume  A in dom fi ; ::_thesis: fi . A is Ordinal
then A1: fi . A in rng fi by FUNCT_1:def_3;
 ex B being Ordinal st rng fi c= B by Def4;
hence  fi . A is Ordinal by A1; ::_thesis: verum
end;

registration
let f be Ordinal-Sequence;
let a be Ordinal;
clusterf . a ->  ordinal ;
coherence
 f . a is ordinal
proof
 ( a in dom f or not a in dom f ) ;
hence  f . a is ordinal by Th25, FUNCT_1:def_2; ::_thesis: verum
end;
end;

scheme :: ORDINAL2:sch 3
OSLambda{ F1() ->  Ordinal, F2( Ordinal) ->  Ordinal } :
 ex fi being Ordinal-Sequence st
( dom fi = F1() & ( for A being Ordinal st A in F1() holds
fi . A = F2(A) ) )
proof
consider L being T-Sequence such that
A1: ( dom L = F1() & ( for A being Ordinal st A in F1() holds
L . A = F2(A) ) ) from ORDINAL2:sch_2();
 L is Ordinal-yielding
proof
take  sup (rng L) ; :: according to ORDINAL2:def_4 ::_thesis: rng L c= sup (rng L)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in sup (rng L) )
assume A2: x in rng L ; ::_thesis: x in sup (rng L)
then consider y being set  such that
A3: y in dom L and
A4: x = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A3;
 L . y = F2(y) by A1, A3;
then A5: x in On (rng L) by A2, A4, ORDINAL1:def_9;
 On (rng L) c= sup (rng L) by Def3;
hence  x in sup (rng L) by A5; ::_thesis: verum
end;
then reconsider L = L as Ordinal-Sequence ;
take fi = L; ::_thesis: ( dom fi = F1() & ( for A being Ordinal st A in F1() holds
fi . A = F2(A) ) )
thus  dom fi = F1() by A1; ::_thesis: for A being Ordinal st A in F1() holds
fi . A = F2(A)
let A be Ordinal; ::_thesis: ( A in F1() implies fi . A = F2(A) )
assume  A in F1() ; ::_thesis: fi . A = F2(A)
hence  fi . A = F2(A) by A1; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 4
TSUniq1{ F1() ->  Ordinal, F2() ->  set , F3( Ordinal, set ) ->  set , F4( Ordinal, T-Sequence) ->  set , F5() ->  T-Sequence, F6() ->  T-Sequence } :
 F5() = F6()
provided
A1: dom F5() = F1() and
A2: ( {} in F1() implies F5() . {} = F2() ) and
A3: for A being Ordinal st succ A in F1() holds
F5() . (succ A) = F3(A,(F5() . A)) and
A4: for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
F5() . A = F4(A,(F5() | A)) and
A5: dom F6() = F1() and
A6: ( {} in F1() implies F6() . {} = F2() ) and
A7: for A being Ordinal st succ A in F1() holds
F6() . (succ A) = F3(A,(F6() . A)) and
A8: for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
F6() . A = F4(A,(F6() | A))
proof
defpred S1[ set ] means F5() . $1 <> F6() . $1;
consider X being set  such that
A9: for Y being set holds
( Y in X iff ( Y in F1() & S1[Y] ) ) from XBOOLE_0:sch_1();
 for b being set st b in X holds
b in F1() by A9;
then A10: X c= F1() by TARSKI:def_3;
assume  F5() <> F6() ; ::_thesis: contradiction
then  ex a being set st
( a in F1() & F5() . a <> F6() . a ) by A1, A5, FUNCT_1:2;
then  X <> {} by A9;
then consider B being Ordinal such that
A11: B in X and
A12: for C being Ordinal st C in X holds
B c= C by A10, ORDINAL1:20;
A13: B in F1() by A9, A11;
then A14: B c= F1() by ORDINAL1:def_2;
then A15: ( dom (F5() | B) = B & dom (F6() | B) = B ) by A1, A5, RELAT_1:62;
A16: now__::_thesis:_for_C_being_Ordinal_st_C_in_B_holds_
F5()_._C_=_F6()_._C
let C be Ordinal; ::_thesis: ( C in B implies F5() . C = F6() . C )
assume A17: C in B ; ::_thesis: F5() . C = F6() . C
then  not C in X by A12, ORDINAL1:5;
hence  F5() . C = F6() . C by A9, A14, A17; ::_thesis: verum
end;
A18: now__::_thesis:_for_a_being_set_st_a_in_B_holds_
(F5()_|_B)_._a_=_(F6()_|_B)_._a
let a be set ; ::_thesis: ( a in B implies (F5() | B) . a = (F6() | B) . a )
assume A19: a in B ; ::_thesis: (F5() | B) . a = (F6() | B) . a
 ( (F5() | B) . a = F5() . a & (F6() | B) . a = F6() . a ) by A15, A19, FUNCT_1:47;
hence  (F5() | B) . a = (F6() | B) . a by A16, A19; ::_thesis: verum
end;
A20: now__::_thesis:_(_ex_C_being_Ordinal_st_B_=_succ_C_implies_F5()_._B_=_F6()_._B_)
given C being Ordinal such that A21: B = succ C ; ::_thesis: F5() . B = F6() . B
A22: ( F5() . C = (F5() | B) . C & F6() . C = (F6() | B) . C ) by A21, FUNCT_1:49, ORDINAL1:6;
 ( F5() . B = F3(C,(F5() . C)) & F6() . B = F3(C,(F6() . C)) ) by A3, A7, A13, A21;
hence  F5() . B = F6() . B by A18, A21, A22, ORDINAL1:6; ::_thesis: verum
end;
now__::_thesis:_(_B_<>_{}_&_(_for_C_being_Ordinal_holds_B_<>_succ_C_)_implies_F5()_._B_=_F6()_._B_)
assume that
A23: B <> {} and
A24: for C being Ordinal holds B <> succ C ; ::_thesis: F5() . B = F6() . B
 B is limit_ordinal by A24, ORDINAL1:29;
then  ( F5() . B = F4(B,(F5() | B)) & F6() . B = F4(B,(F6() | B)) ) by A4, A8, A13, A23;
hence  F5() . B = F6() . B by A15, A18, FUNCT_1:2; ::_thesis: verum
end;
hence  contradiction by A2, A6, A9, A11, A20; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 5
TSExist1{ F1() ->  Ordinal, F2() ->  set , F3( Ordinal, set ) ->  set , F4( Ordinal, T-Sequence) ->  set } :
 ex L being T-Sequence st
( dom L = F1() & ( {} in F1() implies L . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
proof
defpred S1[ Ordinal, T-Sequence] means ( dom $2 = $1 & ( {} in $1 implies $2 . {} = F2() ) & ( for A being Ordinal st succ A in $1 holds
$2 . (succ A) = F3(A,($2 . A)) ) & ( for A being Ordinal st A in $1 & A <> {} & A is limit_ordinal holds
$2 . A = F4(A,($2 | A)) ) );
defpred S2[ Ordinal] means  ex L being T-Sequence st S1[$1,L];
A1: for B being Ordinal st ( for C being Ordinal st C in B holds
S2[C] ) holds
S2[B]
proof
defpred S3[ set , set ] means ( $1 is Ordinal & $2 is T-Sequence & ( for A being Ordinal
for L being T-Sequence st A = $1 & L = $2 holds
S1[A,L] ) );
let B be Ordinal; ::_thesis: ( ( for C being Ordinal st C in B holds
S2[C] ) implies S2[B] )
assume A2: for C being Ordinal st C in B holds
ex L being T-Sequence st S1[C,L] ; ::_thesis: S2[B]
A3: for a, b, c being set st S3[a,b] & S3[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( S3[a,b] & S3[a,c] implies b = c )
assume that
A4: a is Ordinal and
A5: b is T-Sequence and
A6: for A being Ordinal
for L being T-Sequence st A = a & L = b holds
S1[A,L] and
 a is Ordinal and
A7: c is T-Sequence and
A8: for A being Ordinal
for L being T-Sequence st A = a & L = c holds
S1[A,L] ; ::_thesis: b = c
reconsider a = a as Ordinal by A4;
reconsider c = c as T-Sequence by A7;
A9: dom c = a by A8;
A10: for A being Ordinal st A in a & A <> {} & A is limit_ordinal holds
c . A = F4(A,(c | A)) by A8;
A11: for A being Ordinal st succ A in a holds
c . (succ A) = F3(A,(c . A)) by A8;
A12: ( {} in a implies c . {} = F2() ) by A8;
reconsider b = b as T-Sequence by A5;
A13: ( {} in a implies b . {} = F2() ) by A6;
A14: for A being Ordinal st succ A in a holds
b . (succ A) = F3(A,(b . A)) by A6;
A15: for A being Ordinal st A in a & A <> {} & A is limit_ordinal holds
b . A = F4(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 set holds
( [a,b] in G iff ( a in B & S3[a,b] ) ) from FUNCT_1:sch_1(A3);
defpred S4[ set , set ] means  ex A being Ordinal ex L being T-Sequence st
( A = $1 & L = G . $1 & ( ( A = {} & $2 = F2() ) or ex B being Ordinal st
( A = succ B & $2 = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & $2 = F4(A,L) ) ) );
A18: dom G = B
proof
thus  for a being set 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 set ; ::_thesis: ( a in dom G implies a in B )
assume  a in dom G ; ::_thesis: a in B
then  ex b being set st [a,b] in G by XTUPLE_0:def_12;
hence  a in B by A17; ::_thesis: verum
end;
let a be set ; :: 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 T-Sequence such that
A20: S1[a9,L] by A2, A19;
 for A being Ordinal
for K being T-Sequence st A = a9 & K = L holds
S1[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 set st a in B holds
ex b being set st S4[a,b]
proof
let a be set ; ::_thesis: ( a in B implies ex b being set st S4[a,b] )
assume A22: a in B ; ::_thesis: ex b being set st S4[a,b]
then reconsider A = a as Ordinal ;
consider c being set  such that
A23: [a,c] in G by A18, A22, XTUPLE_0:def_12;
reconsider L = c as T-Sequence by A17, A23;
A24: now__::_thesis:_(_ex_C_being_Ordinal_st_A_=_succ_C_implies_ex_b_being_set_st_S4[a,b]_)
given C being Ordinal such that A25: A = succ C ; ::_thesis: ex b being set st S4[a,b]
thus  ex b being set st S4[a,b] ::_thesis: verum
proof
take  F3(C,(L . C)) ; ::_thesis: S4[a,F3(C,(L . C))]
take  A ; ::_thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) )
take  L ; ::_thesis: ( A = a & L = G . a & ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) )
thus  ( A = a & L = G . a ) by A23, FUNCT_1:1; ::_thesis: ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) )
thus  ( ( A = {} & F3(C,(L . C)) = F2() ) or ex B being Ordinal st
( A = succ B & F3(C,(L . C)) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F3(C,(L . C)) = F4(A,L) ) ) by A25; ::_thesis: verum
end;
end;
A26: now__::_thesis:_(_A_<>_{}_&_(_for_C_being_Ordinal_holds_A_<>_succ_C_)_implies_S4[a,F4(A,L)]_)
assume A27: ( A <> {} & ( for C being Ordinal holds A <> succ C ) ) ; ::_thesis: S4[a,F4(A,L)]
thus  S4[a,F4(A,L)] ::_thesis: verum
proof
take  A ; ::_thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) )
take  L ; ::_thesis: ( A = a & L = G . a & ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) )
thus  ( A = a & L = G . a ) by A23, FUNCT_1:1; ::_thesis: ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) )
thus  ( ( A = {} & F4(A,L) = F2() ) or ex B being Ordinal st
( A = succ B & F4(A,L) = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F4(A,L) = F4(A,L) ) ) by A27, ORDINAL1:29; ::_thesis: verum
end;
end;
now__::_thesis:_(_A_=_{}_implies_S4[a,F2()]_)
assume A28: A = {} ; ::_thesis: S4[a,F2()]
thus  S4[a,F2()] ::_thesis: verum
proof
take  A ; ::_thesis: ex L being T-Sequence st
( A = a & L = G . a & ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) )
take  L ; ::_thesis: ( A = a & L = G . a & ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) )
thus  ( A = a & L = G . a ) by A23, FUNCT_1:1; ::_thesis: ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) )
thus  ( ( A = {} & F2() = F2() ) or ex B being Ordinal st
( A = succ B & F2() = F3(B,(L . B)) ) or ( A <> {} & A is limit_ordinal & F2() = F4(A,L) ) ) by A28; ::_thesis: verum
end;
end;
hence  ex b being set st S4[a,b] by A24, A26; ::_thesis: verum
end;
A29: for a, b, c being set st a in B & S4[a,b] & S4[a,c] holds
b = c
proof
let a, b, c be set ; ::_thesis: ( a in B & S4[a,b] & S4[a,c] implies b = c )
assume  a in B ; ::_thesis: ( not S4[a,b] or not S4[a,c] or b = c )
given Ab being Ordinal, Lb being T-Sequence such that A30: Ab = a and
A31: Lb = G . a and
A32: ( ( Ab = {} & b = F2() ) or ex B being Ordinal st
( Ab = succ B & b = F3(B,(Lb . B)) ) or ( Ab <> {} & Ab is limit_ordinal & b = F4(Ab,Lb) ) ) ; ::_thesis: ( not S4[a,c] or b = c )
given Ac being Ordinal, Lc being T-Sequence such that A33: Ac = a and
A34: Lc = G . a and
A35: ( ( Ac = {} & c = F2() ) or ex B being Ordinal st
( Ac = succ B & c = F3(B,(Lc . B)) ) or ( Ac <> {} & Ac is limit_ordinal & c = F4(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 = F3(A,(Lb . A)) by A32, A36, ORDINAL1:29;
consider D being Ordinal such that
A39: Ac = succ D and
A40: c = F3(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 set st a in B holds
S4[a,F . a] ) ) from FUNCT_1:sch_2(A29, A21);
reconsider L = F as T-Sequence by A41, ORDINAL1:def_7;
take  L ; ::_thesis: S1[B,L]
thus  dom L = B by A41; ::_thesis: ( ( {} in B implies L . {} = F2() ) & ( for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
thus  ( {} in B implies L . {} = F2() ) ::_thesis: ( ( for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) )
proof
assume  {} in B ; ::_thesis: L . {} = F2()
then  ex A being Ordinal ex K being T-Sequence st
( A = {} & K = G . {} & ( ( A = {} & F . {} = F2() ) or ex B being Ordinal st
( A = succ B & F . {} = F3(B,(K . B)) ) or ( A <> {} & A is limit_ordinal & F . {} = F4(A,K) ) ) ) by A41;
hence  L . {} = F2() ; ::_thesis: verum
end;
A42: for A being Ordinal
for L1 being T-Sequence st A in B & L1 = G . A holds
L | A = L1
proof
defpred S5[ Ordinal] means  for L1 being T-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
S5[C] ) holds
S5[A]
proof
let A be Ordinal; ::_thesis: ( ( for C being Ordinal st C in A holds
S5[C] ) implies S5[A] )
assume  for C being Ordinal st C in A holds
for L1 being T-Sequence st C in B & L1 = G . C holds
L | C = L1 ; ::_thesis: S5[A]
let L1 be T-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: S1[A,L1] by A17;
A48: now__::_thesis:_for_x_being_set_st_x_in_A_holds_
L1_._x_=_(L_|_A)_._x
let x be set ; ::_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 T-Sequence such that
A51: A1 = x9 and
A52: L2 = G . x9 and
A53: ( ( A1 = {} & L . x9 = F2() ) or ex B being Ordinal st
( A1 = succ B & L . x9 = F3(B,(L2 . B)) ) or ( A1 <> {} & A1 is limit_ordinal & L . x9 = F4(A1,L2) ) ) by A41;
 for D being Ordinal
for L3 being T-Sequence st D = x9 & L3 = L1 | x9 holds
S1[D,L3]
proof
let D be Ordinal; ::_thesis: for L3 being T-Sequence st D = x9 & L3 = L1 | x9 holds
S1[D,L3]
let L3 be T-Sequence; ::_thesis: ( D = x9 & L3 = L1 | x9 implies S1[D,L3] )
assume that
A54: D = x9 and
A55: L3 = L1 | x9 ; ::_thesis: S1[D,L3]
 x9 c= A by A49, ORDINAL1:def_2;
hence  dom L3 = D by A47, A54, A55, RELAT_1:62; ::_thesis: ( ( {} in D implies L3 . {} = F2() ) & ( for A being Ordinal st succ A in D holds
L3 . (succ A) = F3(A,(L3 . A)) ) & ( for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A)) ) )
thus  ( {} in D implies L3 . {} = F2() ) by A47, A49, A54, A55, FUNCT_1:49, ORDINAL1:10; ::_thesis: ( ( for A being Ordinal st succ A in D holds
L3 . (succ A) = F3(A,(L3 . A)) ) & ( for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A)) ) )
thus  for C being Ordinal st succ C in D holds
L3 . (succ C) = F3(C,(L3 . C)) ::_thesis: for A being Ordinal st A in D & A <> {} & A is limit_ordinal holds
L3 . A = F4(A,(L3 | A))
proof
let C be Ordinal; ::_thesis: ( succ C in D implies L3 . (succ C) = F3(C,(L3 . C)) )
assume A56: succ C in D ; ::_thesis: L3 . (succ C) = F3(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) = F3(C,(L3 . C)) by A17, A46, A55, A57; ::_thesis: verum
end;
let C be Ordinal; ::_thesis: ( C in D & C <> {} & C is limit_ordinal implies L3 . C = F4(C,(L3 | C)) )
assume that
A58: C in D and
A59: ( C <> {} & C is limit_ordinal ) ; ::_thesis: L3 . C = F4(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 = F4(C,(L3 | C)) by A17, A46, A59, A60;
hence  L3 . C = F4(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 = F3(D,(L1 . D)) by A17, A46, A49, A63;
consider C being Ordinal such that
A65: A1 = succ C and
A66: L . x9 = F3(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 S5[A] from ORDINAL1:sch_2(A43); ::_thesis: verum
end;
thus  for A being Ordinal st succ A in B holds
L . (succ A) = F3(A,(L . A)) ::_thesis: for A being Ordinal st A in B & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A))
proof
let A be Ordinal; ::_thesis: ( succ A in B implies L . (succ A) = F3(A,(L . A)) )
assume A67: succ A in B ; ::_thesis: L . (succ A) = F3(A,(L . A))
then consider C being Ordinal, K being T-Sequence such that
A68: C = succ A and
A69: K = G . (succ A) and
A70: ( ( C = {} & F . (succ A) = F2() ) or ex B being Ordinal st
( C = succ B & F . (succ A) = F3(B,(K . B)) ) or ( C <> {} & C is limit_ordinal & F . (succ A) = F4(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) = F3(D,(K . D)) by A68, A70, ORDINAL1:29;
 A = D by A68, A72, ORDINAL1:7;
hence  L . (succ A) = F3(A,(L . A)) by A73, A71, FUNCT_1:49, ORDINAL1:6; ::_thesis: verum
end;
let D be Ordinal; ::_thesis: ( D in B & D <> {} & D is limit_ordinal implies L . D = F4(D,(L | D)) )
assume that
A74: D in B and
A75: ( D <> {} & D is limit_ordinal ) ; ::_thesis: L . D = F4(D,(L | D))
 ex A being Ordinal ex K being T-Sequence st
( A = D & K = G . D & ( ( A = {} & F . D = F2() ) or ex B being Ordinal st
( A = succ B & F . D = F3(B,(K . B)) ) or ( A <> {} & A is limit_ordinal & F . D = F4(A,K) ) ) ) by A41, A74;
hence  L . D = F4(D,(L | D)) by A42, A74, A75, ORDINAL1:29; ::_thesis: verum
end;
 for A being Ordinal holds S2[A] from ORDINAL1:sch_2(A1);
hence  ex L being T-Sequence st
( dom L = F1() & ( {} in F1() implies L . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) ) ; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 6
TSResult{ F1() ->  T-Sequence, F2( Ordinal) ->  set , F3() ->  Ordinal, F4() ->  set , F5( Ordinal, set ) ->  set , F6( Ordinal, T-Sequence) ->  set } :
 for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
provided
A1: for A being Ordinal
for x being set holds
( x = F2(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( {} in F3() implies F1() . {} = F4() ) and
A4: for A being Ordinal st succ A in F3() holds
F1() . (succ A) = F5(A,(F1() . A)) and
A5: for A being Ordinal st A in F3() & A <> {} & A is limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proof
let A be Ordinal; ::_thesis: ( A in dom F1() implies F1() . A = F2(A) )
set L = F1() | (succ A);
assume  A in dom F1() ; ::_thesis: F1() . A = F2(A)
then A6: succ A c= dom F1() by ORDINAL1:21;
A7: for C being Ordinal st succ C in succ A holds
(F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
proof
let C be Ordinal; ::_thesis: ( succ C in succ A implies (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) )
assume A8: succ C in succ A ; ::_thesis: (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
 C in succ C by ORDINAL1:6;
then A9: (F1() | (succ A)) . C = F1() . C by A8, FUNCT_1:49, ORDINAL1:10;
 (F1() | (succ A)) . (succ C) = F1() . (succ C) by A8, FUNCT_1:49;
hence  (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) by A2, A4, A6, A8, A9; ::_thesis: verum
end;
A10: for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
(F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
proof
let C be Ordinal; ::_thesis: ( C in succ A & C <> {} & C is limit_ordinal implies (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) )
assume that
A11: C in succ A and
A12: ( C <> {} & C is limit_ordinal ) ; ::_thesis: (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
 C c= succ A by A11, ORDINAL1:def_2;
then A13: (F1() | (succ A)) | C = F1() | C by FUNCT_1:51;
 (F1() | (succ A)) . C = F1() . C by A11, FUNCT_1:49;
hence  (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) by A2, A5, A6, A11, A12, A13; ::_thesis: verum
end;
 {} c= succ A ;
then  {} c< succ A by XBOOLE_0:def_8;
then A14: ( {} in succ A & (F1() | (succ A)) . {} = F1() . {} ) by FUNCT_1:49, ORDINAL1:11;
A15: dom (F1() | (succ A)) = succ A by A6, RELAT_1:62;
then  ( A in succ A & last (F1() | (succ A)) = (F1() | (succ A)) . A ) by Th2, ORDINAL1:21;
then  last (F1() | (succ A)) = F1() . A by FUNCT_1:49;
hence  F1() . A = F2(A) by A1, A2, A3, A6, A15, A14, A7, A10; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 7
TSDef{ F1() ->  Ordinal, F2() ->  set , F3( Ordinal, set ) ->  set , F4( Ordinal, T-Sequence) ->  set } :
 ( ex x being set ex L being T-Sequence st
( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ( for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) holds
x1 = x2 ) )
proof
consider L being T-Sequence such that
A1: ( dom L = succ F1() & ( {} in succ F1() implies L . {} = F2() ) & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) from ORDINAL2:sch_5();
thus  ex x being set ex L being T-Sequence st
( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) ::_thesis: for x1, x2 being set st ex L being T-Sequence st
( x1 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) holds
x1 = x2
proof
take x = last L; ::_thesis: ex L being T-Sequence st
( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
take  L ; ::_thesis: ( x = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
thus  ( x = last L & dom L = succ F1() ) by A1; ::_thesis: ( L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) )
 {} c= succ F1() ;
then  {} c< succ F1() by XBOOLE_0:def_8;
hence  ( L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) by A1, ORDINAL1:11; ::_thesis: verum
end;
let x1, x2 be set ; ::_thesis: ( ex L being T-Sequence st
( x1 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) & ex L being T-Sequence st
( x2 = last L & dom L = succ F1() & L . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) implies x1 = x2 )
given L1 being T-Sequence such that A2: x1 = last L1 and
A3: dom L1 = succ F1() and
A4: L1 . {} = F2() and
A5: for C being Ordinal st succ C in succ F1() holds
L1 . (succ C) = F3(C,(L1 . C)) and
A6: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L1 . C = F4(C,(L1 | C)) ; ::_thesis: ( for L being T-Sequence holds
( not x2 = last L or not dom L = succ F1() or not L . {} = F2() or ex C being Ordinal st
( succ C in succ F1() & not L . (succ C) = F3(C,(L . C)) ) or ex C being Ordinal st
( C in succ F1() & C <> {} & C is limit_ordinal & not L . C = F4(C,(L | C)) ) ) or x1 = x2 )
A7: ( {} in succ F1() implies L1 . {} = F2() ) by A4;
given L2 being T-Sequence such that A8: x2 = last L2 and
A9: dom L2 = succ F1() and
A10: L2 . {} = F2() and
A11: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = F3(C,(L2 . C)) and
A12: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) ; ::_thesis: x1 = x2
A13: ( {} in succ F1() implies L2 . {} = F2() ) by A10;
 L1 = L2 from ORDINAL2:sch_4(A3, A7, A5, A6, A9, A13, A11, A12);
hence  x1 = x2 by A2, A8; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 8
TSResult0{ F1( Ordinal) ->  set , F2() ->  set , F3( Ordinal, set ) ->  set , F4( Ordinal, T-Sequence) ->  set } :
 F1({}) = F2()
provided
A1: for A being Ordinal
for x being set holds
( x = F1(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F2() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F3(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F4(C,(L | C)) ) ) )
proof
consider L being T-Sequence such that
A2: ( dom L = succ {} & ( {} in succ {} implies L . {} = F2() ) & ( for A being Ordinal st succ A in succ {} holds
L . (succ A) = F3(A,(L . A)) ) & ( for A being Ordinal st A in succ {} & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) ) ) from ORDINAL2:sch_5();
 F2() = last L by A2, Th2, ORDINAL1:6;
hence  F1({}) = F2() by A1, A2, ORDINAL1:6; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 9
TSResultS{ F1() ->  set , F2( Ordinal, set ) ->  set , F3( Ordinal, T-Sequence) ->  set , F4( Ordinal) ->  set } :
 for A being Ordinal holds F4((succ A)) = F2(A,F4(A))
provided
A1: for A being Ordinal
for x being set holds
( x = F4(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F1() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F2(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F3(C,(L | C)) ) ) )
proof
let A be Ordinal; ::_thesis: F4((succ A)) = F2(A,F4(A))
consider L being T-Sequence such that
A2: dom L = succ (succ A) and
A3: ( {} in succ (succ A) implies L . {} = F1() ) and
A4: for C being Ordinal st succ C in succ (succ A) holds
L . (succ C) = F2(C,(L . C)) and
A5: for C being Ordinal st C in succ (succ A) & C <> {} & C is limit_ordinal holds
L . C = F3(C,(L | C)) from ORDINAL2:sch_5();
A6: for A being Ordinal
for x being set holds
( x = F4(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F1() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F2(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F3(C,(L | C)) ) ) ) by A1;
A7: for B being Ordinal st B in dom L holds
L . B = F4(B) from ORDINAL2:sch_6(A6, A2, A3, A4, A5);
then A8: L . (succ A) = F4((succ A)) by A2, ORDINAL1:6;
 ( A in succ A & succ A in succ (succ A) ) by ORDINAL1:6;
then  L . A = F4(A) by A2, A7, ORDINAL1:10;
hence  F4((succ A)) = F2(A,F4(A)) by A4, A8, ORDINAL1:6; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 10
TSResultL{ F1() ->  T-Sequence, F2() ->  Ordinal, F3( Ordinal) ->  set , F4() ->  set , F5( Ordinal, set ) ->  set , F6( Ordinal, T-Sequence) ->  set } :
 F3(F2()) = F6(F2(),F1())
provided
A1: for A being Ordinal
for x being set holds
( x = F3(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) and
A2: ( F2() <> {} & F2() is limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proof
A5: F2() in succ F2() by ORDINAL1:6;
consider L being T-Sequence such that
A6: dom L = succ F2() and
A7: ( {} in succ F2() implies L . {} = F4() ) and
A8: for C being Ordinal st succ C in succ F2() holds
L . (succ C) = F5(C,(L . C)) and
A9: for C being Ordinal st C in succ F2() & C <> {} & C is limit_ordinal holds
L . C = F6(C,(L | C)) from ORDINAL2:sch_5();
set L1 = L | F2();
A10: for A being Ordinal
for x being set holds
( x = F3(A) iff ex L being T-Sequence st
( x = last L & dom L = succ A & L . {} = F4() & ( for C being Ordinal st succ C in succ A holds
L . (succ C) = F5(C,(L . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
L . C = F6(C,(L | C)) ) ) ) by A1;
A11: for B being Ordinal st B in dom L holds
L . B = F3(B) from ORDINAL2:sch_6(A10, A6, A7, A8, A9);
A12: now__::_thesis:_for_x_being_set_st_x_in_F2()_holds_
(L_|_F2())_._x_=_F1()_._x
let x be set ; ::_thesis: ( x in F2() implies (L | F2()) . x = F1() . x )
assume A13: x in F2() ; ::_thesis: (L | F2()) . x = F1() . x
then reconsider x9 = x as Ordinal ;
thus (L | F2()) . x = L . x9 by A13, FUNCT_1:49
.= F3(x9) by A6, A11, A5, A13, ORDINAL1:10
.= F1() . x by A4, A13 ; ::_thesis: verum
end;
 F2() c= dom L by A6, A5, ORDINAL1:def_2;
then  dom (L | F2()) = F2() by RELAT_1:62;
then  L | F2() = F1() by A3, A12, FUNCT_1:2;
then  L . F2() = F6(F2(),F1()) by A2, A9, ORDINAL1:6;
hence  F3(F2()) = F6(F2(),F1()) by A6, A11, ORDINAL1:6; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 11
OSExist{ F1() ->  Ordinal, F2() ->  Ordinal, F3( Ordinal, Ordinal) ->  Ordinal, F4( Ordinal, T-Sequence) ->  Ordinal } :
 ex fi being Ordinal-Sequence st
( dom fi = F1() & ( {} in F1() implies fi . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
proof
deffunc H1( Ordinal, set ) ->  Ordinal = F3($1,(sup (union {$2})));
consider L being T-Sequence such that
A1: dom L = F1() and
A2: ( {} in F1() implies L . {} = F2() ) and
A3: for A being Ordinal st succ A in F1() holds
L . (succ A) = H1(A,L . A) and
A4: for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
L . A = F4(A,(L | A)) from ORDINAL2:sch_5();
 L is Ordinal-yielding
proof
take  sup (rng L) ; :: according to ORDINAL2:def_4 ::_thesis: rng L c= sup (rng L)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in sup (rng L) )
assume A5: x in rng L ; ::_thesis: x in sup (rng L)
then consider y being set  such that
A6: y in dom L and
A7: x = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A6;
A8: now__::_thesis:_(_y_<>_{}_&_(_for_B_being_Ordinal_holds_y_<>_succ_B_)_implies_x_is_Ordinal_)
assume that
A9: y <> {} and
A10: for B being Ordinal holds y <> succ B ; ::_thesis: x is Ordinal
 y is limit_ordinal by A10, ORDINAL1:29;
then  L . y = F4(y,(L | y)) by A1, A4, A6, A9;
hence  x is Ordinal by A7; ::_thesis: verum
end;
A11: On (rng L) c= sup (rng L) by Def3;
now__::_thesis:_(_ex_B_being_Ordinal_st_y_=_succ_B_implies_x_is_Ordinal_)
given B being Ordinal such that A12: y = succ B ; ::_thesis: x is Ordinal
 L . y = F3(B,(sup (union {(L . B)}))) by A1, A3, A6, A12;
hence  x is Ordinal by A7; ::_thesis: verum
end;
then  x in On (rng L) by A1, A2, A5, A6, A7, A8, ORDINAL1:def_9;
hence  x in sup (rng L) by A11; ::_thesis: verum
end;
then reconsider L = L as Ordinal-Sequence ;
take fi = L; ::_thesis: ( dom fi = F1() & ( {} in F1() implies fi . {} = F2() ) & ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
thus  ( dom fi = F1() & ( {} in F1() implies fi . {} = F2() ) ) by A1, A2; ::_thesis: ( ( for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) )
thus  for A being Ordinal st succ A in F1() holds
fi . (succ A) = F3(A,(fi . A)) ::_thesis: for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A))
proof
let A be Ordinal; ::_thesis: ( succ A in F1() implies fi . (succ A) = F3(A,(fi . A)) )
reconsider B = fi . A as Ordinal ;
sup (union {B}) = sup B by ZFMISC_1:25
.= B by Th18 ;
hence  ( succ A in F1() implies fi . (succ A) = F3(A,(fi . A)) ) by A3; ::_thesis: verum
end;
thus  for A being Ordinal st A in F1() & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) by A4; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 12
OSResult{ F1() ->  Ordinal-Sequence, F2( Ordinal) ->  Ordinal, F3() ->  Ordinal, F4() ->  Ordinal, F5( Ordinal, Ordinal) ->  Ordinal, F6( Ordinal, T-Sequence) ->  Ordinal } :
 for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
provided
A1: for A, B being Ordinal holds
( B = F2(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: dom F1() = F3() and
A3: ( {} in F3() implies F1() . {} = F4() ) and
A4: for A being Ordinal st succ A in F3() holds
F1() . (succ A) = F5(A,(F1() . A)) and
A5: for A being Ordinal st A in F3() & A <> {} & A is limit_ordinal holds
F1() . A = F6(A,(F1() | A))
proof
let A be Ordinal; ::_thesis: ( A in dom F1() implies F1() . A = F2(A) )
set fi = F1() | (succ A);
assume  A in dom F1() ; ::_thesis: F1() . A = F2(A)
then A6: succ A c= dom F1() by ORDINAL1:21;
A7: for C being Ordinal st succ C in succ A holds
(F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
proof
let C be Ordinal; ::_thesis: ( succ C in succ A implies (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) )
assume A8: succ C in succ A ; ::_thesis: (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C))
 C in succ C by ORDINAL1:6;
then A9: (F1() | (succ A)) . C = F1() . C by A8, FUNCT_1:49, ORDINAL1:10;
 (F1() | (succ A)) . (succ C) = F1() . (succ C) by A8, FUNCT_1:49;
hence  (F1() | (succ A)) . (succ C) = F5(C,((F1() | (succ A)) . C)) by A2, A4, A6, A8, A9; ::_thesis: verum
end;
A10: for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
(F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
proof
let C be Ordinal; ::_thesis: ( C in succ A & C <> {} & C is limit_ordinal implies (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) )
assume that
A11: C in succ A and
A12: ( C <> {} & C is limit_ordinal ) ; ::_thesis: (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C))
 C c= succ A by A11, ORDINAL1:def_2;
then A13: (F1() | (succ A)) | C = F1() | C by FUNCT_1:51;
 (F1() | (succ A)) . C = F1() . C by A11, FUNCT_1:49;
hence  (F1() | (succ A)) . C = F6(C,((F1() | (succ A)) | C)) by A2, A5, A6, A11, A12, A13; ::_thesis: verum
end;
 {} c= succ A ;
then  {} c< succ A by XBOOLE_0:def_8;
then A14: ( {} in succ A & (F1() | (succ A)) . {} = F1() . {} ) by FUNCT_1:49, ORDINAL1:11;
A15: dom (F1() | (succ A)) = succ A by A6, RELAT_1:62;
then  ( A in succ A & last (F1() | (succ A)) = (F1() | (succ A)) . A ) by Th2, ORDINAL1:21;
then  last (F1() | (succ A)) = F1() . A by FUNCT_1:49;
hence  F1() . A = F2(A) by A1, A2, A3, A6, A15, A14, A7, A10; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 13
OSDef{ F1() ->  Ordinal, F2() ->  Ordinal, F3( Ordinal, Ordinal) ->  Ordinal, F4( Ordinal, T-Sequence) ->  Ordinal } :
 ( ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) holds
A1 = A2 ) )
proof
consider fi being Ordinal-Sequence such that
A1: ( dom fi = succ F1() & ( {} in succ F1() implies fi . {} = F2() ) & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) from ORDINAL2:sch_11();
reconsider A = last fi as Ordinal ;
thus  ex A being Ordinal ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) ::_thesis: for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) holds
A1 = A2
proof
take  A ; ::_thesis: ex fi being Ordinal-Sequence st
( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
take  fi ; ::_thesis: ( A = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
thus  ( A = last fi & dom fi = succ F1() ) by A1; ::_thesis: ( fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) )
 {} c= succ F1() ;
then  {} c< succ F1() by XBOOLE_0:def_8;
hence  ( fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) by A1, ORDINAL1:11; ::_thesis: verum
end;
deffunc H1( Ordinal, Ordinal) ->  Ordinal = F3($1,(sup (union {$2})));
let A1, A2 be Ordinal; ::_thesis: ( ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ F1() & fi . {} = F2() & ( for C being Ordinal st succ C in succ F1() holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) implies A1 = A2 )
given L1 being Ordinal-Sequence such that A2: A1 = last L1 and
A3: dom L1 = succ F1() and
A4: L1 . {} = F2() and
A5: for C being Ordinal st succ C in succ F1() holds
L1 . (succ C) = F3(C,(L1 . C)) and
A6: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L1 . C = F4(C,(L1 | C)) ; ::_thesis: ( for fi being Ordinal-Sequence holds
( not A2 = last fi or not dom fi = succ F1() or not fi . {} = F2() or ex C being Ordinal st
( succ C in succ F1() & not fi . (succ C) = F3(C,(fi . C)) ) or ex C being Ordinal st
( C in succ F1() & C <> {} & C is limit_ordinal & not fi . C = F4(C,(fi | C)) ) ) or A1 = A2 )
A7: ( {} in succ F1() implies L1 . {} = F2() ) by A4;
A8: for C being Ordinal st succ C in succ F1() holds
L1 . (succ C) = H1(C,L1 . C)
proof
let C be Ordinal; ::_thesis: ( succ C in succ F1() implies L1 . (succ C) = H1(C,L1 . C) )
assume A9: succ C in succ F1() ; ::_thesis: L1 . (succ C) = H1(C,L1 . C)
reconsider x9 = L1 . C as Ordinal ;
sup (union {(L1 . C)}) = sup x9 by ZFMISC_1:25
.= x9 by Th18 ;
hence  L1 . (succ C) = H1(C,L1 . C) by A5, A9; ::_thesis: verum
end;
given L2 being Ordinal-Sequence such that A10: A2 = last L2 and
A11: dom L2 = succ F1() and
A12: L2 . {} = F2() and
A13: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = F3(C,(L2 . C)) and
A14: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) ; ::_thesis: A1 = A2
A15: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L2 . C = F4(C,(L2 | C)) by A14;
A16: for C being Ordinal st C in succ F1() & C <> {} & C is limit_ordinal holds
L1 . C = F4(C,(L1 | C)) by A6;
A17: for C being Ordinal st succ C in succ F1() holds
L2 . (succ C) = H1(C,L2 . C)
proof
let C be Ordinal; ::_thesis: ( succ C in succ F1() implies L2 . (succ C) = H1(C,L2 . C) )
assume A18: succ C in succ F1() ; ::_thesis: L2 . (succ C) = H1(C,L2 . C)
reconsider x9 = L2 . C as Ordinal ;
sup (union {(L2 . C)}) = sup x9 by ZFMISC_1:25
.= x9 by Th18 ;
hence  L2 . (succ C) = H1(C,L2 . C) by A13, A18; ::_thesis: verum
end;
A19: ( {} in succ F1() implies L2 . {} = F2() ) by A12;
 L1 = L2 from ORDINAL2:sch_4(A3, A7, A8, A16, A11, A19, A17, A15);
hence  A1 = A2 by A2, A10; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 14
OSResult0{ F1( Ordinal) ->  Ordinal, F2() ->  Ordinal, F3( Ordinal, Ordinal) ->  Ordinal, F4( Ordinal, T-Sequence) ->  Ordinal } :
 F1({}) = F2()
provided
A1: for A, B being Ordinal holds
( B = F1(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F2() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F3(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F4(C,(fi | C)) ) ) )
proof
consider fi being Ordinal-Sequence such that
A2: ( dom fi = succ {} & ( {} in succ {} implies fi . {} = F2() ) & ( for A being Ordinal st succ A in succ {} holds
fi . (succ A) = F3(A,(fi . A)) ) & ( for A being Ordinal st A in succ {} & A <> {} & A is limit_ordinal holds
fi . A = F4(A,(fi | A)) ) ) from ORDINAL2:sch_11();
 F2() = last fi by A2, Th2, ORDINAL1:6;
hence  F1({}) = F2() by A1, A2, ORDINAL1:6; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 15
OSResultS{ F1() ->  Ordinal, F2( Ordinal, Ordinal) ->  Ordinal, F3( Ordinal, T-Sequence) ->  Ordinal, F4( Ordinal) ->  Ordinal } :
 for A being Ordinal holds F4((succ A)) = F2(A,F4(A))
provided
A1: for A, B being Ordinal holds
( B = F4(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F1() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F2(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) ) ) )
proof
let A be Ordinal; ::_thesis: F4((succ A)) = F2(A,F4(A))
consider fi being Ordinal-Sequence such that
A2: dom fi = succ (succ A) and
A3: ( {} in succ (succ A) implies fi . {} = F1() ) and
A4: for C being Ordinal st succ C in succ (succ A) holds
fi . (succ C) = F2(C,(fi . C)) and
A5: for C being Ordinal st C in succ (succ A) & C <> {} & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) from ORDINAL2:sch_11();
A6: for A, B being Ordinal holds
( B = F4(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F1() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F2(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F3(C,(fi | C)) ) ) ) by A1;
A7: for B being Ordinal st B in dom fi holds
fi . B = F4(B) from ORDINAL2:sch_12(A6, A2, A3, A4, A5);
then A8: fi . (succ A) = F4((succ A)) by A2, ORDINAL1:6;
 ( A in succ A & succ A in succ (succ A) ) by ORDINAL1:6;
then  fi . A = F4(A) by A2, A7, ORDINAL1:10;
hence  F4((succ A)) = F2(A,F4(A)) by A4, A8, ORDINAL1:6; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 16
OSResultL{ F1() ->  Ordinal-Sequence, F2() ->  Ordinal, F3( Ordinal) ->  Ordinal, F4() ->  Ordinal, F5( Ordinal, Ordinal) ->  Ordinal, F6( Ordinal, T-Sequence) ->  Ordinal } :
 F3(F2()) = F6(F2(),F1())
provided
A1: for A, B being Ordinal holds
( B = F3(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) and
A2: ( F2() <> {} & F2() is limit_ordinal ) and
A3: dom F1() = F2() and
A4: for A being Ordinal st A in F2() holds
F1() . A = F3(A)
proof
A5: F2() in succ F2() by ORDINAL1:6;
consider fi being Ordinal-Sequence such that
A6: dom fi = succ F2() and
A7: ( {} in succ F2() implies fi . {} = F4() ) and
A8: for C being Ordinal st succ C in succ F2() holds
fi . (succ C) = F5(C,(fi . C)) and
A9: for C being Ordinal st C in succ F2() & C <> {} & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) from ORDINAL2:sch_11();
set psi = fi | F2();
A10: for A, B being Ordinal holds
( B = F3(A) iff ex fi being Ordinal-Sequence st
( B = last fi & dom fi = succ A & fi . {} = F4() & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = F5(C,(fi . C)) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = F6(C,(fi | C)) ) ) ) by A1;
A11: for B being Ordinal st B in dom fi holds
fi . B = F3(B) from ORDINAL2:sch_12(A10, A6, A7, A8, A9);
A12: now__::_thesis:_for_x_being_set_st_x_in_F2()_holds_
(fi_|_F2())_._x_=_F1()_._x
let x be set ; ::_thesis: ( x in F2() implies (fi | F2()) . x = F1() . x )
assume A13: x in F2() ; ::_thesis: (fi | F2()) . x = F1() . x
then reconsider x9 = x as Ordinal ;
thus (fi | F2()) . x = fi . x9 by A13, FUNCT_1:49
.= F3(x9) by A6, A11, A5, A13, ORDINAL1:10
.= F1() . x by A4, A13 ; ::_thesis: verum
end;
 F2() c= dom fi by A6, A5, ORDINAL1:def_2;
then  dom (fi | F2()) = F2() by RELAT_1:62;
then  fi | F2() = F1() by A3, A12, FUNCT_1:2;
then  fi . F2() = F6(F2(),F1()) by A2, A9, ORDINAL1:6;
hence  F3(F2()) = F6(F2(),F1()) by A6, A11, ORDINAL1:6; ::_thesis: verum
end;

definition
let L be T-Sequence;
func sup L ->  Ordinal equals :: ORDINAL2:def 5
 sup (rng L);
correctness
coherence
sup (rng L) is Ordinal;
;
func inf L ->  Ordinal equals :: ORDINAL2:def 6
 inf (rng L);
correctness
coherence
inf (rng L) is Ordinal;
;
end;

:: deftheorem  defines sup ORDINAL2:def_5_:_
 for L being T-Sequence holds sup L = sup (rng L);

:: deftheorem  defines inf ORDINAL2:def_6_:_
 for L being T-Sequence holds inf L = inf (rng L);

theorem :: ORDINAL2:26
for L being T-Sequence holds
( sup L = sup (rng L) & inf L = inf (rng L) ) ;

definition
let L be T-Sequence;
func lim_sup L ->  Ordinal means :: ORDINAL2:def 7
 ex fi being Ordinal-Sequence st
( it = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) );
existence
 ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) )
proof
deffunc H1( Ordinal) ->  Ordinal = sup (rng (L | ((dom L) \ $1)));
consider fi being Ordinal-Sequence such that
A1: ( dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = H1(A) ) ) from ORDINAL2:sch_3();
take  inf fi ; ::_thesis: ex fi being Ordinal-Sequence st
( inf fi = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) )
take  fi ; ::_thesis: ( inf fi = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) )
thus  ( inf fi = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( b2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) holds
b1 = b2
proof
let A1, A2 be Ordinal; ::_thesis: ( ex fi being Ordinal-Sequence st
( A1 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( A2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) implies A1 = A2 )
given fi being Ordinal-Sequence such that A2: ( A1 = inf fi & dom fi = dom L ) and
A3: for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ; ::_thesis: ( for fi being Ordinal-Sequence holds
( not A2 = inf fi or not dom fi = dom L or ex A being Ordinal st
( A in dom L & not fi . A = sup (rng (L | ((dom L) \ A))) ) ) or A1 = A2 )
given psi being Ordinal-Sequence such that A4: ( A2 = inf psi & dom psi = dom L ) and
A5: for A being Ordinal st A in dom L holds
psi . A = sup (rng (L | ((dom L) \ A))) ; ::_thesis: A1 = A2
now__::_thesis:_for_x_being_set_st_x_in_dom_L_holds_
fi_._x_=_psi_._x
let x be set ; ::_thesis: ( x in dom L implies fi . x = psi . x )
assume A6: x in dom L ; ::_thesis: fi . x = psi . x
then reconsider A = x as Ordinal ;
 fi . A = sup (rng (L | ((dom L) \ A))) by A3, A6;
hence  fi . x = psi . x by A5, A6; ::_thesis: verum
end;
hence  A1 = A2 by A2, A4, FUNCT_1:2; ::_thesis: verum
end;
func lim_inf L ->  Ordinal means :: ORDINAL2:def 8
 ex fi being Ordinal-Sequence st
( it = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) );
existence
 ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
proof
deffunc H1( Ordinal) ->  Ordinal = inf (rng (L | ((dom L) \ $1)));
consider fi being Ordinal-Sequence such that
A7: ( dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = H1(A) ) ) from ORDINAL2:sch_3();
take  sup fi ; ::_thesis: ex fi being Ordinal-Sequence st
( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
take  fi ; ::_thesis: ( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) )
thus  ( sup fi = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) by A7; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( b2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) holds
b1 = b2
proof
let A1, A2 be Ordinal; ::_thesis: ( ex fi being Ordinal-Sequence st
( A1 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) & ex fi being Ordinal-Sequence st
( A2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) implies A1 = A2 )
given fi being Ordinal-Sequence such that A8: ( A1 = sup fi & dom fi = dom L ) and
A9: for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ; ::_thesis: ( for fi being Ordinal-Sequence holds
( not A2 = sup fi or not dom fi = dom L or ex A being Ordinal st
( A in dom L & not fi . A = inf (rng (L | ((dom L) \ A))) ) ) or A1 = A2 )
given psi being Ordinal-Sequence such that A10: ( A2 = sup psi & dom psi = dom L ) and
A11: for A being Ordinal st A in dom L holds
psi . A = inf (rng (L | ((dom L) \ A))) ; ::_thesis: A1 = A2
now__::_thesis:_for_x_being_set_st_x_in_dom_L_holds_
fi_._x_=_psi_._x
let x be set ; ::_thesis: ( x in dom L implies fi . x = psi . x )
assume A12: x in dom L ; ::_thesis: fi . x = psi . x
then reconsider A = x as Ordinal ;
 fi . A = inf (rng (L | ((dom L) \ A))) by A9, A12;
hence  fi . x = psi . x by A11, A12; ::_thesis: verum
end;
hence  A1 = A2 by A8, A10, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem  defines lim_sup ORDINAL2:def_7_:_
 for L being T-Sequence
for b2 being Ordinal holds
( b2 = lim_sup L iff ex fi being Ordinal-Sequence st
( b2 = inf fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = sup (rng (L | ((dom L) \ A))) ) ) );

:: deftheorem  defines lim_inf ORDINAL2:def_8_:_
 for L being T-Sequence
for b2 being Ordinal holds
( b2 = lim_inf L iff ex fi being Ordinal-Sequence st
( b2 = sup fi & dom fi = dom L & ( for A being Ordinal st A in dom L holds
fi . A = inf (rng (L | ((dom L) \ A))) ) ) );

definition
let A be Ordinal;
let fi be Ordinal-Sequence;
predA is_limes_of fi means :Def9: :: ORDINAL2:def 9
 ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) if A = {}
otherwise  for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) );
consistency
 verum ;
end;

:: deftheorem Def9 defines is_limes_of ORDINAL2:def_9_:_
 for A being Ordinal
for fi being Ordinal-Sequence holds
( ( A = {} implies ( A is_limes_of fi iff ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) ) & ( not A = {} implies ( A is_limes_of fi iff for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) );

definition
let fi be Ordinal-Sequence;
given A being Ordinal such that A1: A is_limes_of fi ;
func lim fi ->  Ordinal means :Def10: :: ORDINAL2:def 10
it is_limes_of fi;
existence
 ex b1 being Ordinal st b1 is_limes_of fi by A1;
uniqueness
 for b1, b2 being Ordinal st b1 is_limes_of fi & b2 is_limes_of fi holds
b1 = b2
proof
let A1, A2 be Ordinal; ::_thesis: ( A1 is_limes_of fi & A2 is_limes_of fi implies A1 = A2 )
assume that
A2: ( ( A1 = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A1 <> {} & ( for B, C being Ordinal st B in A1 & A1 in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) ) and
A3: ( ( A2 = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A2 <> {} & ( for B, C being Ordinal st B in A2 & A2 in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def_9 ::_thesis: A1 = A2
A4: now__::_thesis:_not_A1_in_A2
set x = the Element of A1;
reconsider x = the Element of A1 as Ordinal ;
assume  A1 in A2 ; ::_thesis: contradiction
then consider D being Ordinal such that
A5: D in dom fi and
A6: for A being Ordinal st D c= A & A in dom fi holds
( A1 in fi . A & fi . A in succ A2 ) by A3, ORDINAL1:6;
now__::_thesis:_not_A1_=_{}
assume  A1 = {} ; ::_thesis: contradiction
then consider B being Ordinal such that
A7: B in dom fi and
A8: for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} by A2;
 ( B c= D or D c= B ) ;
then consider E being Ordinal such that
A9: ( ( E = D & B c= D ) or ( E = B & D c= B ) ) ;
 fi . E = {} by A5, A7, A8, A9;
hence  contradiction by A5, A6, A7, A9; ::_thesis: verum
end;
then consider C being Ordinal such that
A10: C in dom fi and
A11: for A being Ordinal st C c= A & A in dom fi holds
( x in fi . A & fi . A in succ A1 ) by A2, ORDINAL1:6;
 ( C c= D or D c= C ) ;
then consider E being Ordinal such that
A12: ( ( E = D & C c= D ) or ( E = C & D c= C ) ) ;
 fi . E in succ A1 by A5, A10, A11, A12;
then A13: ( fi . E in A1 or fi . E = A1 ) by ORDINAL1:8;
 A1 in fi . E by A5, A6, A10, A12;
hence  contradiction by A13; ::_thesis: verum
end;
set x = the Element of A2;
reconsider x = the Element of A2 as Ordinal ;
assume  A1 <> A2 ; ::_thesis: contradiction
then  ( A1 in A2 or A2 in A1 ) by ORDINAL1:14;
then consider D being Ordinal such that
A14: D in dom fi and
A15: for A being Ordinal st D c= A & A in dom fi holds
( A2 in fi . A & fi . A in succ A1 ) by A2, A4, ORDINAL1:6;
now__::_thesis:_not_A2_=_{}
assume  A2 = {} ; ::_thesis: contradiction
then consider B being Ordinal such that
A16: B in dom fi and
A17: for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} by A3;
 ( B c= D or D c= B ) ;
then consider E being Ordinal such that
A18: ( ( E = D & B c= D ) or ( E = B & D c= B ) ) ;
 fi . E = {} by A14, A16, A17, A18;
hence  contradiction by A14, A15, A16, A18; ::_thesis: verum
end;
then consider C being Ordinal such that
A19: C in dom fi and
A20: for A being Ordinal st C c= A & A in dom fi holds
( x in fi . A & fi . A in succ A2 ) by A3, ORDINAL1:6;
 ( C c= D or D c= C ) ;
then consider E being Ordinal such that
A21: ( ( E = D & C c= D ) or ( E = C & D c= C ) ) ;
 fi . E in succ A2 by A14, A19, A20, A21;
then A22: ( fi . E in A2 or fi . E = A2 ) by ORDINAL1:8;
 A2 in fi . E by A14, A15, A19, A21;
hence  contradiction by A22; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines lim ORDINAL2:def_10_:_
 for fi being Ordinal-Sequence st ex A being Ordinal st A is_limes_of fi holds
for b2 being Ordinal holds
( b2 = lim fi iff b2 is_limes_of fi );

definition
let A be Ordinal;
let fi be Ordinal-Sequence;
func lim (A,fi) ->  Ordinal equals :: ORDINAL2:def 11
 lim (fi | A);
correctness
coherence
lim (fi | A) is Ordinal;
;
end;

:: deftheorem  defines lim ORDINAL2:def_11_:_
 for A being Ordinal
for fi being Ordinal-Sequence holds lim (A,fi) = lim (fi | A);

definition
let L be Ordinal-Sequence;
attrL is increasing  means :: ORDINAL2:def 12
 for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B;
attrL is continuous  means :: ORDINAL2:def 13
 for A, B being Ordinal st A in dom L & A <> {} & A is limit_ordinal & B = L . A holds
B is_limes_of L | A;
end;

:: deftheorem  defines increasing ORDINAL2:def_12_:_
 for L being Ordinal-Sequence holds
( L is increasing iff for A, B being Ordinal st A in B & B in dom L holds
L . A in L . B );

:: deftheorem  defines continuous ORDINAL2:def_13_:_
 for L being Ordinal-Sequence holds
( L is continuous iff for A, B being Ordinal st A in dom L & A <> {} & A is limit_ordinal & B = L . A holds
B is_limes_of L | A );

definition
let A, B be Ordinal;
funcA +^ B ->  Ordinal means :Def14: :: ORDINAL2:def 14
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, T-Sequence) ->  Ordinal = sup $2;
deffunc H2( Ordinal, Ordinal) ->  set = succ $2;
 ( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
hence  ( ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) & ( for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def14 defines +^ ORDINAL2:def_14_:_
 for A, B, b3 being Ordinal holds
( b3 = A +^ B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = succ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = sup (fi | C) ) ) );

definition
let A, B be Ordinal;
funcA *^ B ->  Ordinal means :Def15: :: ORDINAL2:def 15
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, Ordinal-Sequence) ->  set = union (sup $2);
deffunc H2( Ordinal, Ordinal) ->  Ordinal = $2 +^ B;
 ( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
hence  ( ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ( for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def15 defines *^ ORDINAL2:def_15_:_
 for A, B, b3 being Ordinal holds
( b3 = A *^ B iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ A & fi . {} = {} & ( for C being Ordinal st succ C in succ A holds
fi . (succ C) = (fi . C) +^ B ) & ( for C being Ordinal st C in succ A & C <> {} & C is limit_ordinal holds
fi . C = union (sup (fi | C)) ) ) );

registration
let O be Ordinal;
cluster  ->  ordinal for Element of O;
coherence
 for b1 being Element of O holds b1 is ordinal ;
end;

definition
let A, B be Ordinal;
func exp (A,B) ->  Ordinal means :Def16: :: ORDINAL2:def 16
 ex fi being Ordinal-Sequence st
( it = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) );
correctness
existence
ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) );
uniqueness
for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, Ordinal-Sequence) ->  Ordinal = lim $2;
deffunc H2( Ordinal, Ordinal) ->  Ordinal = A *^ $2;
 ( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
hence  ( ex b1 being Ordinal ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ( for b1, b2 being Ordinal st ex fi being Ordinal-Sequence st
( b1 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) & ex fi being Ordinal-Sequence st
( b2 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def16 defines exp ORDINAL2:def_16_:_
 for A, B, b3 being Ordinal holds
( b3 = exp (A,B) iff ex fi being Ordinal-Sequence st
( b3 = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = A *^ (fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = lim (fi | C) ) ) );

theorem Th27: :: ORDINAL2:27
for A being Ordinal holds A +^ {} = A
proof
let A be Ordinal; ::_thesis: A +^ {} = A
deffunc H1( Ordinal, Ordinal) ->  set = succ $2;
deffunc H2( Ordinal, T-Sequence) ->  Ordinal = sup $2;
deffunc H3( Ordinal) ->  Ordinal = A +^ $1;
A1: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) ) by Def14;
thus  H3( {} ) = A from ORDINAL2:sch_14(A1); ::_thesis: verum
end;

theorem Th28: :: ORDINAL2:28
for A, B being Ordinal holds A +^ (succ B) = succ (A +^ B)
proof
let A, B be Ordinal; ::_thesis: A +^ (succ B) = succ (A +^ B)
deffunc H1( Ordinal, Ordinal) ->  set = succ $2;
deffunc H2( Ordinal, T-Sequence) ->  Ordinal = sup $2;
deffunc H3( Ordinal) ->  Ordinal = A +^ $1;
A1: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) ) by Def14;
 for B being Ordinal holds H3( succ B) = H1(B,H3(B)) from ORDINAL2:sch_15(A1);
hence  A +^ (succ B) = succ (A +^ B) ; ::_thesis: verum
end;

theorem Th29: :: ORDINAL2:29
for B, A being Ordinal st B <> {} & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) holds
A +^ B = sup fi
proof
let B, A be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) holds
A +^ B = sup fi )
deffunc H1( Ordinal, Ordinal) ->  set = succ $2;
deffunc H2( Ordinal, Ordinal-Sequence) ->  Ordinal = sup $2;
assume A1: ( B <> {} & B is limit_ordinal ) ; ::_thesis: for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) holds
A +^ B = sup fi
deffunc H3( Ordinal) ->  Ordinal = A +^ $1;
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = B & ( for C being Ordinal st C in B holds
fi . C = A +^ C ) implies A +^ B = sup fi )
assume that
A2: dom fi = B and
A3: for C being Ordinal st C in B holds
fi . C = H3(C) ; ::_thesis: A +^ B = sup fi
A4: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = A & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) ) by Def14;
thus  H3(B) = H2(B,fi) from ORDINAL2:sch_16(A4, A1, A2, A3); ::_thesis: verum
end;

theorem Th30: :: ORDINAL2:30
for A being Ordinal holds {} +^ A = A
proof
let A be Ordinal; ::_thesis: {} +^ A = A
defpred S1[ Ordinal] means {} +^ $1 = $1;
A1: for A being Ordinal st S1[A] holds
S1[ succ A] by Th28;
A2: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
deffunc H1( Ordinal) ->  Ordinal = {} +^ $1;
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A3: ( A <> {} & A is limit_ordinal ) and
A4: for B being Ordinal st B in A holds
{} +^ B = B ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A5: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
A6: rng fi = A
proof
thus  for x being set st x in rng fi holds
x in A :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A c= rng fi
proof
let x be set ; ::_thesis: ( x in rng fi implies x in A )
assume  x in rng fi ; ::_thesis: x in A
then consider y being set  such that
A7: y in dom fi and
A8: x = fi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A7;
x = {} +^ y by A5, A7, A8
.= y by A4, A5, A7 ;
hence  x in A by A5, A7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng fi )
assume A9: x in A ; ::_thesis: x in rng fi
then reconsider B = x as Ordinal ;
 ( {} +^ B = B & fi . B = {} +^ B ) by A4, A5, A9;
hence  x in rng fi by A5, A9, FUNCT_1:def_3; ::_thesis: verum
end;
{} +^ A = sup fi by A3, A5, Th29
.= sup (rng fi) ;
hence  S1[A] by A6, Th18; ::_thesis: verum
end;
A10: S1[ {} ] by Th27;
 for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A10, A1, A2);
hence  {} +^ A = A ; ::_thesis: verum
end;

Lm1:  1 = succ {}
;

theorem :: ORDINAL2:31
for A being Ordinal holds A +^ 1 = succ A
proof
let A be Ordinal; ::_thesis: A +^ 1 = succ A
thus A +^ 1 = succ (A +^ {}) by Lm1, Th28
.= succ A by Th27 ; ::_thesis: verum
end;

theorem Th32: :: ORDINAL2:32
for A, B, C being Ordinal st A in B holds
C +^ A in C +^ B
proof
let A, B, C be Ordinal; ::_thesis: ( A in B implies C +^ A in C +^ B )
defpred S1[ Ordinal] means ( A in $1 implies C +^ A in C +^ $1 );
A1: for B being Ordinal st ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A2: for D being Ordinal st D in B & A in D holds
C +^ A in C +^ D and
A3: A in B ; ::_thesis: C +^ A in C +^ B
A4: now__::_thesis:_(_ex_D_being_Ordinal_st_B_=_succ_D_implies_C_+^_A_in_C_+^_B_)
given D being Ordinal such that A5: B = succ D ; ::_thesis: C +^ A in C +^ B
A6: now__::_thesis:_(_A_in_D_implies_C_+^_A_in_C_+^_B_)
assume  A in D ; ::_thesis: C +^ A in C +^ B
then A7: C +^ A in C +^ D by A2, A5, ORDINAL1:6;
 ( succ (C +^ D) = C +^ (succ D) & C +^ D in succ (C +^ D) ) by Th28, ORDINAL1:6;
hence  C +^ A in C +^ B by A5, A7, ORDINAL1:10; ::_thesis: verum
end;
now__::_thesis:_(_not_A_in_D_implies_C_+^_A_in_C_+^_B_)
assume A8: not A in D ; ::_thesis: C +^ A in C +^ B
 ( A c< D iff ( A c= D & A <> D ) ) by XBOOLE_0:def_8;
then  C +^ A in succ (C +^ D) by A3, A5, A8, ORDINAL1:11, ORDINAL1:22;
hence  C +^ A in C +^ B by A5, Th28; ::_thesis: verum
end;
hence  C +^ A in C +^ B by A6; ::_thesis: verum
end;
now__::_thesis:_(_(_for_D_being_Ordinal_holds_B_<>_succ_D_)_implies_C_+^_A_in_C_+^_B_)
deffunc H1( Ordinal) ->  Ordinal = C +^ $1;
consider fi being Ordinal-Sequence such that
A9: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
 fi . A = C +^ A by A3, A9;
then A10: C +^ A in rng fi by A3, A9, FUNCT_1:def_3;
assume  for D being Ordinal holds B <> succ D ; ::_thesis: C +^ A in C +^ B
then  B is limit_ordinal by ORDINAL1:29;
then C +^ B = sup fi by A3, A9, Th29
.= sup (rng fi) ;
hence  C +^ A in C +^ B by A10, Th19; ::_thesis: verum
end;
hence  C +^ A in C +^ B by A4; ::_thesis: verum
end;
 for B being Ordinal holds S1[B] from ORDINAL1:sch_2(A1);
hence  ( A in B implies C +^ A in C +^ B ) ; ::_thesis: verum
end;

theorem Th33: :: ORDINAL2:33
for A, B, C being Ordinal st A c= B holds
C +^ A c= C +^ B
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies C +^ A c= C +^ B )
assume A1: A c= B ; ::_thesis: C +^ A c= C +^ B
now__::_thesis:_(_A_<>_B_implies_C_+^_A_c=_C_+^_B_)
assume  A <> B ; ::_thesis: C +^ A c= C +^ B
then  A c< B by A1, XBOOLE_0:def_8;
then  C +^ A in C +^ B by Th32, ORDINAL1:11;
hence  C +^ A c= C +^ B by ORDINAL1:def_2; ::_thesis: verum
end;
hence  C +^ A c= C +^ B ; ::_thesis: verum
end;

theorem Th34: :: ORDINAL2:34
for A, B, C being Ordinal st A c= B holds
A +^ C c= B +^ C
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies A +^ C c= B +^ C )
defpred S1[ Ordinal] means A +^ $1 c= B +^ $1;
assume A1: A c= B ; ::_thesis: A +^ C c= B +^ C
A2: for C being Ordinal st ( for D being Ordinal st D in C holds
S1[D] ) holds
S1[C]
proof
let C be Ordinal; ::_thesis: ( ( for D being Ordinal st D in C holds
S1[D] ) implies S1[C] )
assume A3: for D being Ordinal st D in C holds
A +^ D c= B +^ D ; ::_thesis: S1[C]
A4: now__::_thesis:_(_ex_D_being_Ordinal_st_C_=_succ_D_implies_S1[C]_)
given D being Ordinal such that A5: C = succ D ; ::_thesis: S1[C]
A6: B +^ C = succ (B +^ D) by A5, Th28;
 ( A +^ D c= B +^ D & A +^ C = succ (A +^ D) ) by A3, A5, Th28, ORDINAL1:6;
hence  S1[C] by A6, Th1; ::_thesis: verum
end;
A7: now__::_thesis:_(_C_<>_{}_&_(_for_D_being_Ordinal_holds_C_<>_succ_D_)_implies_S1[C]_)
deffunc H1( Ordinal) ->  Ordinal = A +^ $1;
assume that
A8: C <> {} and
A9: for D being Ordinal holds C <> succ D ; ::_thesis: S1[C]
consider fi being Ordinal-Sequence such that
A10: ( dom fi = C & ( for D being Ordinal st D in C holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
A11: now__::_thesis:_for_D_being_Ordinal_st_D_in_rng_fi_holds_
D_in_B_+^_C
let D be Ordinal; ::_thesis: ( D in rng fi implies D in B +^ C )
assume  D in rng fi ; ::_thesis: D in B +^ C
then consider x being set  such that
A12: x in dom fi and
A13: D = fi . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A12;
A14: B +^ x in B +^ C by A10, A12, Th32;
 ( D = A +^ x & A +^ x c= B +^ x ) by A3, A10, A12, A13;
hence  D in B +^ C by A14, ORDINAL1:12; ::_thesis: verum
end;
 C is limit_ordinal by A9, ORDINAL1:29;
then A +^ C = sup fi by A8, A10, Th29
.= sup (rng fi) ;
hence  S1[C] by A11, Th20; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_S1[C]_)
assume A15: C = {} ; ::_thesis: S1[C]
then  A +^ C = A by Th27;
hence  S1[C] by A1, A15, Th27; ::_thesis: verum
end;
hence  S1[C] by A4, A7; ::_thesis: verum
end;
 for C being Ordinal holds S1[C] from ORDINAL1:sch_2(A2);
hence  A +^ C c= B +^ C ; ::_thesis: verum
end;

theorem Th35: :: ORDINAL2:35
for A being Ordinal holds {} *^ A = {}
proof
let A be Ordinal; ::_thesis: {} *^ A = {}
deffunc H1( Ordinal, T-Sequence) ->  set = union (sup $2);
deffunc H2( Ordinal) ->  Ordinal = $1 *^ A;
deffunc H3( Ordinal, Ordinal) ->  Ordinal = $2 +^ A;
A1: for B, C being Ordinal holds
( C = H2(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = {} & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H3(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def15;
thus  H2( {} ) = {} from ORDINAL2:sch_14(A1); ::_thesis: verum
end;

theorem Th36: :: ORDINAL2:36
for B, A being Ordinal holds (succ B) *^ A = (B *^ A) +^ A
proof
let B, A be Ordinal; ::_thesis: (succ B) *^ A = (B *^ A) +^ A
deffunc H1( Ordinal, T-Sequence) ->  set = union (sup $2);
deffunc H2( Ordinal) ->  Ordinal = $1 *^ A;
deffunc H3( Ordinal, Ordinal) ->  Ordinal = $2 +^ A;
A1: for B, C being Ordinal holds
( C = H2(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = {} & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H3(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def15;
 for B being Ordinal holds H2( succ B) = H3(B,H2(B)) from ORDINAL2:sch_15(A1);
hence  (succ B) *^ A = (B *^ A) +^ A ; ::_thesis: verum
end;

theorem Th37: :: ORDINAL2:37
for B, A being Ordinal st B <> {} & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) holds
B *^ A = union (sup fi)
proof
let B, A be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) holds
B *^ A = union (sup fi) )
deffunc H1( Ordinal, Ordinal-Sequence) ->  set = union (sup $2);
assume A1: ( B <> {} & B is limit_ordinal ) ; ::_thesis: for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) holds
B *^ A = union (sup fi)
deffunc H2( Ordinal, Ordinal) ->  Ordinal = $2 +^ A;
deffunc H3( Ordinal) ->  Ordinal = $1 *^ A;
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = B & ( for C being Ordinal st C in B holds
fi . C = C *^ A ) implies B *^ A = union (sup fi) )
assume that
A2: dom fi = B and
A3: for C being Ordinal st C in B holds
fi . C = H3(C) ; ::_thesis: B *^ A = union (sup fi)
A4: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = {} & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def15;
thus  H3(B) = H1(B,fi) from ORDINAL2:sch_16(A4, A1, A2, A3); ::_thesis: verum
end;

theorem Th38: :: ORDINAL2:38
for A being Ordinal holds A *^ {} = {}
proof
let A be Ordinal; ::_thesis: A *^ {} = {}
defpred S1[ Ordinal] means $1 *^ {} = {} ;
A1: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume  A *^ {} = {} ; ::_thesis: S1[ succ A]
hence (succ A) *^ {} = {} +^ {} by Th36
.= {} by Th27 ;
::_thesis: verum
end;
A2: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
deffunc H1( Ordinal) ->  Ordinal = $1 *^ {};
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A3: A <> {} and
A4: A is limit_ordinal and
A5: for B being Ordinal st B in A holds
B *^ {} = {} ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
 rng fi = succ {}
proof
thus  for x being set st x in rng fi holds
x in succ {} :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: succ {} c= rng fi
proof
let x be set ; ::_thesis: ( x in rng fi implies x in succ {} )
assume  x in rng fi ; ::_thesis: x in succ {}
then consider y being set  such that
A7: y in dom fi and
A8: x = fi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A7;
x = y *^ {} by A6, A7, A8
.= {} by A5, A6, A7 ;
hence  x in succ {} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in succ {} or x in rng fi )
assume  x in succ {} ; ::_thesis: x in rng fi
then A9: x = {} by TARSKI:def_1;
 {} c= A ;
then A10: {} c< A by A3, XBOOLE_0:def_8;
then A11: {} in A by ORDINAL1:11;
 {} *^ {} = {} by Th35;
then  fi . x = x by A6, A10, A9, ORDINAL1:11;
hence  x in rng fi by A6, A11, A9, FUNCT_1:def_3; ::_thesis: verum
end;
then A12: sup (rng fi) = succ {} by Th18;
A *^ {} = union (sup fi) by A3, A4, A6, Th37
.= union (sup (rng fi)) ;
hence  S1[A] by A12, Th2; ::_thesis: verum
end;
A13: S1[ {} ] by Th35;
 for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A13, A1, A2);
hence  A *^ {} = {} ; ::_thesis: verum
end;

theorem Th39: :: ORDINAL2:39
for A being Ordinal holds
( 1 *^ A = A & A *^ 1 = A )
proof
let A be Ordinal; ::_thesis: ( 1 *^ A = A & A *^ 1 = A )
defpred S1[ Ordinal] means $1 *^ (succ {}) = $1;
thus 1 *^ A = ({} *^ A) +^ A by Lm1, Th36
.= {} +^ A by Th35
.= A by Th30 ; ::_thesis: A *^ 1 = A
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2: for B being Ordinal st B in A holds
B *^ (succ {}) = B ; ::_thesis: S1[A]
A3: now__::_thesis:_(_A_<>_{}_&_(_for_B_being_Ordinal_holds_A_<>_succ_B_)_implies_A_*^_(succ_{})_=_A_)
deffunc H1( Ordinal) ->  Ordinal = $1 *^ (succ {});
assume that
A4: A <> {} and
A5: for B being Ordinal holds A <> succ B ; ::_thesis: A *^ (succ {}) = A
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for D being Ordinal st D in A holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
A7: A = rng fi
proof
thus  A c= rng fi :: according to XBOOLE_0:def_10 ::_thesis: rng fi c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in rng fi )
assume A8: x in A ; ::_thesis: x in rng fi
then reconsider B = x as Ordinal ;
x = B *^ (succ {}) by A2, A8
.= fi . x by A6, A8 ;
hence  x in rng fi by A6, A8, FUNCT_1:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng fi or x in A )
assume  x in rng fi ; ::_thesis: x in A
then consider y being set  such that
A9: y in dom fi and
A10: x = fi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A9;
fi . y = y *^ (succ {}) by A6, A9
.= y by A2, A6, A9 ;
hence  x in A by A6, A9, A10; ::_thesis: verum
end;
A11: A is limit_ordinal by A5, ORDINAL1:29;
then A *^ (succ {}) = union (sup fi) by A4, A6, Th37
.= union (sup (rng fi)) ;
hence A *^ (succ {}) = union A by A7, Th18
.= A by A11, ORDINAL1:def_6 ;
::_thesis: verum
end;
now__::_thesis:_(_ex_B_being_Ordinal_st_A_=_succ_B_implies_A_*^_(succ_{})_=_A_)
given B being Ordinal such that A12: A = succ B ; ::_thesis: A *^ (succ {}) = A
thus A *^ (succ {}) = (B *^ (succ {})) +^ (succ {}) by A12, Th36
.= B +^ (succ {}) by A2, A12, ORDINAL1:6
.= succ (B +^ {}) by Th28
.= A by A12, Th27 ; ::_thesis: verum
end;
hence  S1[A] by A3, Th35; ::_thesis: verum
end;
 for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1);
hence  A *^ 1 = A ; ::_thesis: verum
end;

theorem Th40: :: ORDINAL2:40
for C, A, B being Ordinal st C <> {} & A in B holds
A *^ C in B *^ C
proof
let C, A, B be Ordinal; ::_thesis: ( C <> {} & A in B implies A *^ C in B *^ C )
A1: {} c= C ;
defpred S1[ Ordinal] means ( A in $1 implies A *^ C in $1 *^ C );
assume  C <> {} ; ::_thesis: ( not A in B or A *^ C in B *^ C )
then A2: {} c< C by A1, XBOOLE_0:def_8;
then A3: {} in C by ORDINAL1:11;
A4: for B being Ordinal st ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
let B be Ordinal; ::_thesis: ( ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A5: for D being Ordinal st D in B & A in D holds
A *^ C in D *^ C and
A6: A in B ; ::_thesis: A *^ C in B *^ C
A7: now__::_thesis:_(_ex_D_being_Ordinal_st_B_=_succ_D_implies_A_*^_C_in_B_*^_C_)
given D being Ordinal such that A8: B = succ D ; ::_thesis: A *^ C in B *^ C
A9: now__::_thesis:_(_A_in_D_implies_A_*^_C_in_B_*^_C_)
assume  A in D ; ::_thesis: A *^ C in B *^ C
then A10: A *^ C in D *^ C by A5, A8, ORDINAL1:6;
A11: (D *^ C) +^ {} in (D *^ C) +^ C by A2, Th32, ORDINAL1:11;
 ( (D *^ C) +^ C = (succ D) *^ C & (D *^ C) +^ {} = D *^ C ) by Th27, Th36;
hence  A *^ C in B *^ C by A8, A10, A11, ORDINAL1:10; ::_thesis: verum
end;
now__::_thesis:_(_not_A_in_D_implies_A_*^_C_in_B_*^_C_)
A12: (A *^ C) +^ {} = A *^ C by Th27;
assume A13: not A in D ; ::_thesis: A *^ C in B *^ C
 ( A c< D iff ( A c= D & A <> D ) ) by XBOOLE_0:def_8;
then  (A *^ C) +^ {} in (D *^ C) +^ C by A3, A6, A8, A13, Th32, ORDINAL1:11, ORDINAL1:22;
hence  A *^ C in B *^ C by A8, A12, Th36; ::_thesis: verum
end;
hence  A *^ C in B *^ C by A9; ::_thesis: verum
end;
now__::_thesis:_(_(_for_D_being_Ordinal_holds_B_<>_succ_D_)_implies_A_*^_C_in_B_*^_C_)
A14: ( (A *^ C) +^ {} = A *^ C & (A *^ C) +^ {} in (A *^ C) +^ C ) by A2, Th27, Th32, ORDINAL1:11;
A15: (succ A) *^ C = (A *^ C) +^ C by Th36;
deffunc H1( Ordinal) ->  Ordinal = $1 *^ C;
consider fi being Ordinal-Sequence such that
A16: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
assume  for D being Ordinal holds B <> succ D ; ::_thesis: A *^ C in B *^ C
then A17: B is limit_ordinal by ORDINAL1:29;
then A18: succ A in B by A6, ORDINAL1:28;
then  fi . (succ A) = (succ A) *^ C by A16;
then  (succ A) *^ C in rng fi by A16, A18, FUNCT_1:def_3;
then A19: (succ A) *^ C c= union (sup (rng fi)) by Th19, ZFMISC_1:74;
B *^ C = union (sup fi) by A6, A17, A16, Th37
.= union (sup (rng fi)) ;
hence  A *^ C in B *^ C by A19, A14, A15; ::_thesis: verum
end;
hence  A *^ C in B *^ C by A7; ::_thesis: verum
end;
 for B being Ordinal holds S1[B] from ORDINAL1:sch_2(A4);
hence  ( not A in B or A *^ C in B *^ C ) ; ::_thesis: verum
end;

theorem :: ORDINAL2:41
for A, B, C being Ordinal st A c= B holds
A *^ C c= B *^ C
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies A *^ C c= B *^ C )
assume A1: A c= B ; ::_thesis: A *^ C c= B *^ C
A2: now__::_thesis:_(_C_<>_{}_implies_A_*^_C_c=_B_*^_C_)
assume A3: C <> {} ; ::_thesis: A *^ C c= B *^ C
now__::_thesis:_(_A_<>_B_implies_A_*^_C_c=_B_*^_C_)
assume  A <> B ; ::_thesis: A *^ C c= B *^ C
then  A c< B by A1, XBOOLE_0:def_8;
then  A *^ C in B *^ C by A3, Th40, ORDINAL1:11;
hence  A *^ C c= B *^ C by ORDINAL1:def_2; ::_thesis: verum
end;
hence  A *^ C c= B *^ C ; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_A_*^_C_c=_B_*^_C_)
assume  C = {} ; ::_thesis: A *^ C c= B *^ C
then  A *^ C = {} by Th38;
hence  A *^ C c= B *^ C ; ::_thesis: verum
end;
hence  A *^ C c= B *^ C by A2; ::_thesis: verum
end;

theorem :: ORDINAL2:42
for A, B, C being Ordinal st A c= B holds
C *^ A c= C *^ B
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies C *^ A c= C *^ B )
assume A1: A c= B ; ::_thesis: C *^ A c= C *^ B
now__::_thesis:_(_B_<>_{}_implies_C_*^_A_c=_C_*^_B_)
defpred S1[ Ordinal] means $1 *^ A c= $1 *^ B;
assume A2: B <> {} ; ::_thesis: C *^ A c= C *^ B
A3: for C being Ordinal st ( for D being Ordinal st D in C holds
S1[D] ) holds
S1[C]
proof
let C be Ordinal; ::_thesis: ( ( for D being Ordinal st D in C holds
S1[D] ) implies S1[C] )
assume A4: for D being Ordinal st D in C holds
D *^ A c= D *^ B ; ::_thesis: S1[C]
A5: now__::_thesis:_(_ex_D_being_Ordinal_st_C_=_succ_D_implies_S1[C]_)
given D being Ordinal such that A6: C = succ D ; ::_thesis: S1[C]
 D *^ A c= D *^ B by A4, A6, ORDINAL1:6;
then A7: (D *^ A) +^ A c= (D *^ B) +^ A by Th34;
A8: ( C *^ A = (D *^ A) +^ A & C *^ B = (D *^ B) +^ B ) by A6, Th36;
 (D *^ B) +^ A c= (D *^ B) +^ B by A1, Th33;
hence  S1[C] by A7, A8, XBOOLE_1:1; ::_thesis: verum
end;
A9: now__::_thesis:_(_C_<>_{}_&_(_for_D_being_Ordinal_holds_C_<>_succ_D_)_implies_S1[C]_)
deffunc H1( Ordinal) ->  Ordinal = $1 *^ A;
assume that
A10: C <> {} and
A11: for D being Ordinal holds C <> succ D ; ::_thesis: S1[C]
consider fi being Ordinal-Sequence such that
A12: ( dom fi = C & ( for D being Ordinal st D in C holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
now__::_thesis:_for_D_being_Ordinal_st_D_in_rng_fi_holds_
D_in_C_*^_B
let D be Ordinal; ::_thesis: ( D in rng fi implies D in C *^ B )
assume  D in rng fi ; ::_thesis: D in C *^ B
then consider x being set  such that
A13: x in dom fi and
A14: D = fi . x by FUNCT_1:def_3;
reconsider x = x as Ordinal by A13;
A15: x *^ B in C *^ B by A2, A12, A13, Th40;
 ( D = x *^ A & x *^ A c= x *^ B ) by A4, A12, A13, A14;
hence  D in C *^ B by A15, ORDINAL1:12; ::_thesis: verum
end;
then A16: sup (rng fi) c= C *^ B by Th20;
 C is limit_ordinal by A11, ORDINAL1:29;
then A17: C *^ A = union (sup fi) by A10, A12, Th37
.= union (sup (rng fi)) ;
 union (sup (rng fi)) c= sup (rng fi) by Th5;
hence  S1[C] by A17, A16, XBOOLE_1:1; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_S1[C]_)
assume  C = {} ; ::_thesis: S1[C]
then  C *^ A = {} by Th35;
hence  S1[C] ; ::_thesis: verum
end;
hence  S1[C] by A5, A9; ::_thesis: verum
end;
 for C being Ordinal holds S1[C] from ORDINAL1:sch_2(A3);
hence  C *^ A c= C *^ B ; ::_thesis: verum
end;
hence  C *^ A c= C *^ B by A1; ::_thesis: verum
end;

theorem Th43: :: ORDINAL2:43
for A being Ordinal holds exp (A,{}) = 1
proof
let A be Ordinal; ::_thesis: exp (A,{}) = 1
deffunc H1( Ordinal, Ordinal-Sequence) ->  Ordinal = lim $2;
deffunc H2( Ordinal) ->  Ordinal = exp (A,$1);
deffunc H3( Ordinal, Ordinal) ->  Ordinal = A *^ $2;
A1: for B, C being Ordinal holds
( C = H2(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H3(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def16;
thus  H2( {} ) = 1 from ORDINAL2:sch_14(A1); ::_thesis: verum
end;

theorem Th44: :: ORDINAL2:44
for A, B being Ordinal holds exp (A,(succ B)) = A *^ (exp (A,B))
proof
let A, B be Ordinal; ::_thesis: exp (A,(succ B)) = A *^ (exp (A,B))
deffunc H1( Ordinal, Ordinal-Sequence) ->  Ordinal = lim $2;
deffunc H2( Ordinal) ->  Ordinal = exp (A,$1);
deffunc H3( Ordinal, Ordinal) ->  Ordinal = A *^ $2;
A1: for B, C being Ordinal holds
( C = H2(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H3(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def16;
 for B being Ordinal holds H2( succ B) = H3(B,H2(B)) from ORDINAL2:sch_15(A1);
hence  exp (A,(succ B)) = A *^ (exp (A,B)) ; ::_thesis: verum
end;

theorem Th45: :: ORDINAL2:45
for B, A being Ordinal st B <> {} & B is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) holds
exp (A,B) = lim fi
proof
let B, A be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) holds
exp (A,B) = lim fi )
deffunc H1( Ordinal, Ordinal-Sequence) ->  Ordinal = lim $2;
assume A1: ( B <> {} & B is limit_ordinal ) ; ::_thesis: for fi being Ordinal-Sequence st dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) holds
exp (A,B) = lim fi
deffunc H2( Ordinal, Ordinal) ->  Ordinal = A *^ $2;
deffunc H3( Ordinal) ->  Ordinal = exp (A,$1);
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = B & ( for C being Ordinal st C in B holds
fi . C = exp (A,C) ) implies exp (A,B) = lim fi )
assume that
A2: dom fi = B and
A3: for C being Ordinal st C in B holds
fi . C = H3(C) ; ::_thesis: exp (A,B) = lim fi
A4: for B, C being Ordinal holds
( C = H3(B) iff ex fi being Ordinal-Sequence st
( C = last fi & dom fi = succ B & fi . {} = 1 & ( for C being Ordinal st succ C in succ B holds
fi . (succ C) = H2(C,fi . C) ) & ( for C being Ordinal st C in succ B & C <> {} & C is limit_ordinal holds
fi . C = H1(C,fi | C) ) ) ) by Def16;
thus  H3(B) = H1(B,fi) from ORDINAL2:sch_16(A4, A1, A2, A3); ::_thesis: verum
end;

theorem :: ORDINAL2:46
for A being Ordinal holds
( exp (A,1) = A & exp (1,A) = 1 )
proof
let A be Ordinal; ::_thesis: ( exp (A,1) = A & exp (1,A) = 1 )
defpred S1[ Ordinal] means  exp (1,$1) = 1;
A1: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume  exp (1,A) = 1 ; ::_thesis: S1[ succ A]
hence  exp (1,(succ A)) = 1 *^ 1 by Th44
.= 1 by Th39 ;
::_thesis: verum
end;
thus  exp (A,1) = A *^ (exp (A,{})) by Lm1, Th44
.= A *^ 1 by Th43
.= A by Th39 ; ::_thesis: exp (1,A) = 1
A2: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
deffunc H1( Ordinal) ->  Ordinal = exp (1,$1);
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A3: A <> {} and
A4: A is limit_ordinal and
A5: for B being Ordinal st B in A holds
exp (1,B) = 1 ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
A7: rng fi c= {1}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng fi or x in {1} )
assume  x in rng fi ; ::_thesis: x in {1}
then consider y being set  such that
A8: y in dom fi and
A9: x = fi . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A8;
x = exp (1,y) by A6, A8, A9
.= 1 by A5, A6, A8 ;
hence  x in {1} by TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_(_{}_<>_1_&_(_for_B,_C_being_Ordinal_st_B_in_1_&_1_in_C_holds_
ex_D_being_Ordinal_st_
(_D_in_dom_fi_&_(_for_E_being_Ordinal_st_D_c=_E_&_E_in_dom_fi_holds_
(_B_in_fi_._E_&_fi_._E_in_C_)_)_)_)_)
set x = the Element of A;
thus  {} <> 1 ; ::_thesis: for B, C being Ordinal st B in 1 & 1 in C holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) )
let B, C be Ordinal; ::_thesis: ( B in 1 & 1 in C implies ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) ) )
assume A10: ( B in 1 & 1 in C ) ; ::_thesis: ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) )
reconsider x = the Element of A as Ordinal ;
take D = x; ::_thesis: ( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C ) ) )
thus  D in dom fi by A3, A6; ::_thesis: for E being Ordinal st D c= E & E in dom fi holds
( B in fi . E & fi . E in C )
let E be Ordinal; ::_thesis: ( D c= E & E in dom fi implies ( B in fi . E & fi . E in C ) )
assume that
 D c= E and
A11: E in dom fi ; ::_thesis: ( B in fi . E & fi . E in C )
 fi . E in rng fi by A11, FUNCT_1:def_3;
hence  ( B in fi . E & fi . E in C ) by A7, A10, TARSKI:def_1; ::_thesis: verum
end;
then A12: 1 is_limes_of fi by Def9;
 exp (1,A) = lim fi by A3, A4, A6, Th45;
hence  S1[A] by A12, Def10; ::_thesis: verum
end;
A13: S1[ {} ] by Th43;
 for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A13, A1, A2);
hence  exp (1,A) = 1 ; ::_thesis: verum
end;

theorem :: ORDINAL2:47
for A being Ordinal ex B, C being Ordinal st
( B is limit_ordinal & C is natural & A = B +^ C )
proof
defpred S1[ Ordinal] means  ex B, C being Ordinal st
( B is limit_ordinal & C is natural & $1 = B +^ C );
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A2: for B being Ordinal st B in A holds
S1[B] ; ::_thesis: S1[A]
A3: ( ex B being Ordinal st A = succ B implies S1[A] )
proof
given B being Ordinal such that A4: A = succ B ; ::_thesis: S1[A]
consider C, D being Ordinal such that
A5: C is limit_ordinal and
A6: D is natural and
A7: B = C +^ D by A2, A4, ORDINAL1:6;
take  C ; ::_thesis: ex C being Ordinal st
( C is limit_ordinal & C is natural & A = C +^ C )
take E = succ D; ::_thesis: ( C is limit_ordinal & E is natural & A = C +^ E )
thus  C is limit_ordinal by A5; ::_thesis: ( E is natural & A = C +^ E )
thus  E in omega by A6, ORDINAL1:def_12; :: according to ORDINAL1:def_12 ::_thesis: A = C +^ E
thus  A = C +^ E by A4, A7, Th28; ::_thesis: verum
end;
 ( ( for B being Ordinal holds A <> succ B ) implies S1[A] )
proof
assume A8: for D being Ordinal holds A <> succ D ; ::_thesis: S1[A]
take B = A; ::_thesis: ex C being Ordinal st
( B is limit_ordinal & C is natural & A = B +^ C )
take C = {} ; ::_thesis: ( B is limit_ordinal & C is natural & A = B +^ C )
thus  B is limit_ordinal by A8, ORDINAL1:29; ::_thesis: ( C is natural & A = B +^ C )
thus  C in omega by ORDINAL1:def_11; :: according to ORDINAL1:def_12 ::_thesis: A = B +^ C
thus  A = B +^ C by Th27; ::_thesis: verum
end;
hence  S1[A] by A3; ::_thesis: verum
end;
thus  for A being Ordinal holds S1[A] from ORDINAL1:sch_2(A1); ::_thesis: verum
end;

registration
let X be set ;
let o be Ordinal;
clusterX --> o ->  Ordinal-yielding ;
coherence
 X --> o is Ordinal-yielding
proof
 ( rng (X --> o) c= {o} & {o} c= succ o ) by FUNCOP_1:13, XBOOLE_1:7;
then  rng (X --> o) c= succ o by XBOOLE_1:1;
hence  X --> o is Ordinal-yielding by Def4; ::_thesis: verum
end;
end;

registration
let O be Ordinal;
let x be set ;
clusterO --> x ->  T-Sequence-like ;
coherence
 O --> x is T-Sequence-like
proof
 dom (O --> x) = O by FUNCOP_1:13;
hence  O --> x is T-Sequence-like by ORDINAL1:def_7; ::_thesis: verum
end;
end;

definition
let A, B be Ordinal;
predA is_cofinal_with B means :: ORDINAL2:def 17
 ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi );
reflexivity
 for A being Ordinal ex xi being Ordinal-Sequence st
( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
proof
let A be Ordinal; ::_thesis: ex xi being Ordinal-Sequence st
( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
A1: dom (id A) = A by RELAT_1:45;
then reconsider xi = id A as T-Sequence by ORDINAL1:def_7;
A2: rng (id A) = A by RELAT_1:45;
then reconsider xi = xi as Ordinal-Sequence by Def4;
take  xi ; ::_thesis: ( dom xi = A & rng xi c= A & xi is increasing & A = sup xi )
thus  ( dom xi = A & rng xi c= A ) by RELAT_1:45; ::_thesis: ( xi is increasing & A = sup xi )
thus  xi is increasing ::_thesis: A = sup xi
proof
let B be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for B being Ordinal st B in B & B in dom xi holds
xi . B in xi . B
let C be Ordinal; ::_thesis: ( B in C & C in dom xi implies xi . B in xi . C )
assume that
A3: B in C and
A4: C in dom xi ; ::_thesis: xi . B in xi . C
 xi . C = C by A1, A4, FUNCT_1:18;
hence  xi . B in xi . C by A1, A3, A4, FUNCT_1:18, ORDINAL1:10; ::_thesis: verum
end;
thus  A = sup xi by A2, Th18; ::_thesis: verum
end;
end;

:: deftheorem  defines is_cofinal_with ORDINAL2:def_17_:_
 for A, B being Ordinal holds
( A is_cofinal_with B iff ex xi being Ordinal-Sequence st
( dom xi = B & rng xi c= A & xi is increasing & A = sup xi ) );


theorem Th48: :: ORDINAL2:48
for psi being Ordinal-Sequence
for e being set st e in rng psi holds
e is Ordinal
proof
let psi be Ordinal-Sequence; ::_thesis: for e being set st e in rng psi holds
e is Ordinal
let e be set ; ::_thesis: ( e in rng psi implies e is Ordinal )
assume  e in rng psi ; ::_thesis: e is Ordinal
then  ex u being set st
( u in dom psi & e = psi . u ) by FUNCT_1:def_3;
hence  e is Ordinal ; ::_thesis: verum
end;

theorem :: ORDINAL2:49
for psi being Ordinal-Sequence holds rng psi c= sup psi
proof
let psi be Ordinal-Sequence; ::_thesis: rng psi c= sup psi
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng psi or e in sup psi )
assume A1: e in rng psi ; ::_thesis: e in sup psi
then  e is Ordinal by Th48;
hence  e in sup psi by A1, Th19; ::_thesis: verum
end;

theorem :: ORDINAL2:50
for A being Ordinal st A is_cofinal_with {} holds
A = {}
proof
let A be Ordinal; ::_thesis: ( A is_cofinal_with {} implies A = {} )
given psi being Ordinal-Sequence such that A1: dom psi = {} and
 rng psi c= A and
 psi is increasing and
A2: A = sup psi ; :: according to ORDINAL2:def_17 ::_thesis: A = {}
thus A = sup {} by A1, A2, RELAT_1:42
.= {} by Th18 ; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 17
OmegaInd{ F1() ->  Nat, P1[ set ] } :
 P1[F1()]
provided
A1: P1[ {} ] and
A2: for a being Nat st P1[a] holds
P1[ succ a]
proof
defpred S1[ Ordinal] means ( $1 is natural implies P1[$1] );
A3: now__::_thesis:_for_A_being_Ordinal_st_S1[A]_holds_
S1[_succ_A]
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume A4: S1[A] ; ::_thesis: S1[ succ A]
now__::_thesis:_(_succ_A_is_natural_implies_S1[_succ_A]_)
assume  succ A is natural ; ::_thesis: S1[ succ A]
then A5: succ A in omega by ORDINAL1:def_12;
 A in succ A by ORDINAL1:6;
then  A is Element of omega by A5, ORDINAL1:10;
hence  S1[ succ A] by A2, A4; ::_thesis: verum
end;
hence  S1[ succ A] ; ::_thesis: verum
end;
A6: now__::_thesis:_for_A_being_Ordinal_st_A_<>_{}_&_A_is_limit_ordinal_&_(_for_B_being_Ordinal_st_B_in_A_holds_
S1[B]_)_holds_
S1[A]
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume A7: A <> {} ; ::_thesis: ( A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
 {} c= A ;
then  {} c< A by A7, XBOOLE_0:def_8;
then A8: {} in A by ORDINAL1:11;
A9: not A in A ;
assume  A is limit_ordinal ; ::_thesis: ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
then  omega c= A by A8, ORDINAL1:def_11;
then  not A in omega by A9;
hence  ( ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] ) by ORDINAL1:def_12; ::_thesis: verum
end;
A10: S1[ {} ] by A1;
 for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A10, A3, A6);
hence  P1[F1()] ; ::_thesis: verum
end;

registration
let a, b be Nat;
clustera +^ b ->  natural ;
coherence
 a +^ b is natural
proof
defpred S1[ Nat] means a +^ a is natural ;
A1: now__::_thesis:_for_b_being_Nat_st_S1[b]_holds_
S1[_succ_b]
let b be Nat; ::_thesis: ( S1[b] implies S1[ succ b] )
assume  S1[b] ; ::_thesis: S1[ succ b]
then reconsider c = a +^ b as Nat ;
 a +^ (succ b) = succ c by Th28;
hence  S1[ succ b] ; ::_thesis: verum
end;
A2: S1[ {} ] by Th27;
thus  S1[b] from ORDINAL2:sch_17(A2, A1); ::_thesis: verum
end;
end;

registration
let x, y be set ;
let a, b be Nat;
cluster IFEQ (x,y,a,b) ->  natural ;
coherence
 IFEQ (x,y,a,b) is natural
proof
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: IFEQ (x,y,a,b) is natural
hence  IFEQ (x,y,a,b) is natural by FUNCOP_1:def_8; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: IFEQ (x,y,a,b) is natural
hence  IFEQ (x,y,a,b) is natural by FUNCOP_1:def_8; ::_thesis: verum
end;
end;
end;
end;

scheme :: ORDINAL2:sch 18
LambdaRecEx{ F1() ->  set , F2( set , set ) ->  set } :
 ex f being Function st
( dom f = omega & f . {} = F1() & ( for n being Nat holds f . (succ n) = F2(n,(f . n)) ) )
proof
deffunc H1( set , set ) ->  set = {} ;
consider L being T-Sequence such that
A1: dom L = omega and
A2: ( {} in omega implies L . {} = F1() ) and
A3: for A being Ordinal st succ A in omega holds
L . (succ A) = F2(A,(L . A)) and
 for A being Ordinal st A in omega & A <> {} & A is limit_ordinal holds
L . A = H1(A,L | A) from ORDINAL2:sch_5();
take  L ; ::_thesis: ( dom L = omega & L . {} = F1() & ( for n being Nat holds L . (succ n) = F2(n,(L . n)) ) )
thus  dom L = omega by A1; ::_thesis: ( L . {} = F1() & ( for n being Nat holds L . (succ n) = F2(n,(L . n)) ) )
 {} in omega by ORDINAL1:def_12;
hence  L . {} = F1() by A2; ::_thesis: for n being Nat holds L . (succ n) = F2(n,(L . n))
let n be Nat; ::_thesis: L . (succ n) = F2(n,(L . n))
 succ n in omega by ORDINAL1:def_12;
hence  L . (succ n) = F2(n,(L . n)) by A3; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 19
RecUn{ F1() ->  set , F2() ->  Function, F3() ->  Function, P1[ set , set , set ] } :
 F2() = F3()
provided
A1: dom F2() = omega and
A2: F2() . {} = F1() and
A3: for n being Nat holds P1[n,F2() . n,F2() . (succ n)] and
A4: dom F3() = omega and
A5: F3() . {} = F1() and
A6: for n being Nat holds P1[n,F3() . n,F3() . (succ n)] and
A7: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof
defpred S1[ Nat] means F2() . $1 = F3() . $1;
A8: for n being Nat st S1[n] holds
S1[ succ n]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[ succ n] )
assume  F2() . n = F3() . n ; ::_thesis: S1[ succ n]
then A9: P1[n,F2() . n,F3() . (succ n)] by A6;
 P1[n,F2() . n,F2() . (succ n)] by A3;
hence  S1[ succ n] by A7, A9; ::_thesis: verum
end;
A10: S1[ {} ] by A2, A5;
 for n being Nat holds S1[n]
proof
let n be Nat; ::_thesis: S1[n]
thus  S1[n] from ORDINAL2:sch_17(A10, A8); ::_thesis: verum
end;
then  for x being set st x in omega holds
F2() . x = F3() . x ;
hence  F2() = F3() by A1, A4, FUNCT_1:2; ::_thesis: verum
end;

scheme :: ORDINAL2:sch 20
LambdaRecUn{ F1() ->  set , F2( set , set ) ->  set , F3() ->  Function, F4() ->  Function } :
 F3() = F4()
provided
A1: dom F3() = omega and
A2: F3() . {} = F1() and
A3: for n being Nat holds F3() . (succ n) = F2(n,(F3() . n)) and
A4: dom F4() = omega and
A5: F4() . {} = F1() and
A6: for n being Nat holds F4() . (succ n) = F2(n,(F4() . n))
proof
defpred S1[ Nat, set , set ] means $3 = F2($1,$2);
A7: for n being Nat holds S1[n,F4() . n,F4() . (succ n)] by A6;
A8: for n being Nat
for x, y1, y2 being set st S1[n,x,y1] & S1[n,x,y2] holds
y1 = y2 ;
A9: for n being Nat holds S1[n,F3() . n,F3() . (succ n)] by A3;
thus  F3() = F4() from ORDINAL2:sch_19(A1, A2, A9, A4, A5, A7, A8); ::_thesis: verum
end;