:: ORDINAL3 semantic presentation

begin


theorem :: ORDINAL3:1
for X being set holds X c= succ X by XBOOLE_1:7;

theorem :: ORDINAL3:2
for X, Y being set st succ X c= Y holds
X c= Y
proof
let X, Y be set ; ::_thesis: ( succ X c= Y implies X c= Y )
 X c= succ X by XBOOLE_1:7;
hence  ( succ X c= Y implies X c= Y ) by XBOOLE_1:1; ::_thesis: verum
end;

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

theorem :: ORDINAL3:4
for A being Ordinal
for X being set st X c= A holds
union X is Ordinal
proof
let A be Ordinal; ::_thesis: for X being set st X c= A holds
union X is Ordinal
let X be set ; ::_thesis: ( X c= A implies union X is Ordinal )
assume  X c= A ; ::_thesis: union X is Ordinal
then  for x being set st x in X holds
x is Ordinal ;
hence  union X is Ordinal by ORDINAL1:23; ::_thesis: verum
end;

theorem Th5: :: ORDINAL3:5
for X being set holds union (On X) is Ordinal
proof
let X be set ; ::_thesis: union (On X) is Ordinal
 for x being set st x in On X holds
x is Ordinal by ORDINAL1:def_9;
hence  union (On X) is Ordinal by ORDINAL1:23; ::_thesis: verum
end;

theorem Th6: :: ORDINAL3:6
for A being Ordinal
for X being set st X c= A holds
On X = X
proof
let A be Ordinal; ::_thesis: for X being set st X c= A holds
On X = X
let X be set ; ::_thesis: ( X c= A implies On X = X )
defpred S1[ set ] means ( $1 in X & $1 is Ordinal );
assume  X c= A ; ::_thesis: On X = X
then A1: for x being set holds
( x in X iff S1[x] ) ;
A2: for x being set holds
( x in On X iff S1[x] ) by ORDINAL1:def_9;
thus  On X = X from XBOOLE_0:sch_2(A2, A1); ::_thesis: verum
end;

theorem Th7: :: ORDINAL3:7
for A being Ordinal holds On {A} = {A}
proof
let A be Ordinal; ::_thesis: On {A} = {A}
 {A} c= succ A by XBOOLE_1:7;
hence  On {A} = {A} by Th6; ::_thesis: verum
end;

theorem Th8: :: ORDINAL3:8
for A being Ordinal st A <> {} holds
{} in A
proof
let A be Ordinal; ::_thesis: ( A <> {} implies {} in A )
A1: {} c= A by XBOOLE_1:2;
assume  A <> {} ; ::_thesis: {} in A
then  {} c< A by A1, XBOOLE_0:def_8;
hence  {} in A by ORDINAL1:11; ::_thesis: verum
end;

theorem :: ORDINAL3:9
for A being Ordinal holds inf A = {}
proof
let A be Ordinal; ::_thesis: inf A = {}
A1: inf A = meet A by ORDINAL2:8;
then  ( A <> {} implies inf A = {} ) by Th8, SETFAM_1:4;
hence  inf A = {} by A1, SETFAM_1:def_1; ::_thesis: verum
end;

theorem :: ORDINAL3:10
for A being Ordinal holds inf {A} = A
proof
let A be Ordinal; ::_thesis: inf {A} = A
thus  inf {A} = meet {A} by Th7
.= A by SETFAM_1:10 ; ::_thesis: verum
end;

theorem :: ORDINAL3:11
for A being Ordinal
for X being set st X c= A holds
meet X is Ordinal
proof
let A be Ordinal; ::_thesis: for X being set st X c= A holds
meet X is Ordinal
let X be set ; ::_thesis: ( X c= A implies meet X is Ordinal )
assume  X c= A ; ::_thesis: meet X is Ordinal
then  inf X = meet X by Th6;
hence  meet X is Ordinal ; ::_thesis: verum
end;

registration
let A, B be Ordinal;
clusterA \/ B ->  ordinal ;
coherence
 A \/ B is ordinal
proof
 ( A c= B or B c= A ) ;
hence  A \/ B is ordinal by XBOOLE_1:12; ::_thesis: verum
end;
clusterA /\ B ->  ordinal ;
coherence
 A /\ B is ordinal
proof
 ( A c= B or B c= A ) ;
hence  A /\ B is ordinal by XBOOLE_1:28; ::_thesis: verum
end;
end;

theorem :: ORDINAL3:12
for A, B being Ordinal holds
( A \/ B = A or A \/ B = B )
proof
let A, B be Ordinal; ::_thesis: ( A \/ B = A or A \/ B = B )
 ( A c= B or B c= A ) ;
hence  ( A \/ B = A or A \/ B = B ) by XBOOLE_1:12; ::_thesis: verum
end;

theorem :: ORDINAL3:13
for A, B being Ordinal holds
( A /\ B = A or A /\ B = B )
proof
let A, B be Ordinal; ::_thesis: ( A /\ B = A or A /\ B = B )
 ( A c= B or B c= A ) ;
hence  ( A /\ B = A or A /\ B = B ) by XBOOLE_1:28; ::_thesis: verum
end;

Lm1:  1 = succ {}
;

theorem Th14: :: ORDINAL3:14
for A being Ordinal st A in 1 holds
A = {}
proof
let A be Ordinal; ::_thesis: ( A in 1 implies A = {} )
assume  A in 1 ; ::_thesis: A = {}
hence  ( A c= {} & {} c= A ) by Lm1, ORDINAL1:22, XBOOLE_1:2; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem :: ORDINAL3:15
1 = {{}} by Lm1;

theorem Th16: :: ORDINAL3:16
for A being Ordinal holds
( not A c= 1 or A = {} or A = 1 )
proof
let A be Ordinal; ::_thesis: ( not A c= 1 or A = {} or A = 1 )
assume that
A1: A c= 1 and
A2: A <> {} and
A3: A <> 1 ; ::_thesis: contradiction
 A c< 1 by A1, A3, XBOOLE_0:def_8;
hence  contradiction by A2, Th14, ORDINAL1:11; ::_thesis: verum
end;

theorem :: ORDINAL3:17
for A, B, C, D being Ordinal st ( A c= B or A in B ) & C in D holds
A +^ C in B +^ D
proof
let A, B, C, D be Ordinal; ::_thesis: ( ( A c= B or A in B ) & C in D implies A +^ C in B +^ D )
assume that
A1: ( A c= B or A in B ) and
A2: C in D ; ::_thesis: A +^ C in B +^ D
A3: B +^ C in B +^ D by A2, ORDINAL2:32;
 A c= B by A1, ORDINAL1:def_2;
hence  A +^ C in B +^ D by A3, ORDINAL1:12, ORDINAL2:34; ::_thesis: verum
end;

theorem :: ORDINAL3:18
for A, B, C, D being Ordinal st A c= B & C c= D holds
A +^ C c= B +^ D
proof
let A, B, C, D be Ordinal; ::_thesis: ( A c= B & C c= D implies A +^ C c= B +^ D )
assume that
A1: A c= B and
A2: C c= D ; ::_thesis: A +^ C c= B +^ D
A3: B +^ C c= B +^ D by A2, ORDINAL2:33;
 A +^ C c= B +^ C by A1, ORDINAL2:34;
hence  A +^ C c= B +^ D by A3, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th19: :: ORDINAL3:19
for A, B, C, D being Ordinal st A in B & ( ( C c= D & D <> {} ) or C in D ) holds
A *^ C in B *^ D
proof
let A, B, C, D be Ordinal; ::_thesis: ( A in B & ( ( C c= D & D <> {} ) or C in D ) implies A *^ C in B *^ D )
assume that
A1: A in B and
A2: ( ( C c= D & D <> {} ) or C in D ) ; ::_thesis: A *^ C in B *^ D
A3: C c= D by A2, ORDINAL1:def_2;
 A *^ D in B *^ D by A1, A2, ORDINAL2:40;
hence  A *^ C in B *^ D by A3, ORDINAL1:12, ORDINAL2:42; ::_thesis: verum
end;

theorem :: ORDINAL3:20
for A, B, C, D being Ordinal st A c= B & C c= D holds
A *^ C c= B *^ D
proof
let A, B, C, D be Ordinal; ::_thesis: ( A c= B & C c= D implies A *^ C c= B *^ D )
assume that
A1: A c= B and
A2: C c= D ; ::_thesis: A *^ C c= B *^ D
A3: B *^ C c= B *^ D by A2, ORDINAL2:42;
 A *^ C c= B *^ C by A1, ORDINAL2:41;
hence  A *^ C c= B *^ D by A3, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th21: :: ORDINAL3:21
for B, C, D being Ordinal st B +^ C = B +^ D holds
C = D
proof
let B, C, D be Ordinal; ::_thesis: ( B +^ C = B +^ D implies C = D )
assume that
A1: B +^ C = B +^ D and
A2: C <> D ; ::_thesis: contradiction
 ( C in D or D in C ) by A2, ORDINAL1:14;
then  B +^ C in B +^ C by A1, ORDINAL2:32;
hence  contradiction ; ::_thesis: verum
end;

theorem Th22: :: ORDINAL3:22
for B, C, D being Ordinal st B +^ C in B +^ D holds
C in D
proof
let B, C, D be Ordinal; ::_thesis: ( B +^ C in B +^ D implies C in D )
assume that
A1: B +^ C in B +^ D and
A2: not C in D ; ::_thesis: contradiction
 D c= C by A2, ORDINAL1:16;
hence  contradiction by A1, ORDINAL1:5, ORDINAL2:33; ::_thesis: verum
end;

theorem Th23: :: ORDINAL3:23
for B, C, D being Ordinal st B +^ C c= B +^ D holds
C c= D
proof
let B, C, D be Ordinal; ::_thesis: ( B +^ C c= B +^ D implies C c= D )
assume A1: B +^ C c= B +^ D ; ::_thesis: C c= D
 ( ( B +^ C c= B +^ D & B +^ C <> B +^ D ) iff B +^ C c< B +^ D ) by XBOOLE_0:def_8;
then  ( C = D or C in D ) by A1, Th21, Th22, ORDINAL1:11;
hence  C c= D by ORDINAL1:def_2; ::_thesis: verum
end;

theorem Th24: :: ORDINAL3:24
for A, B being Ordinal holds
( A c= A +^ B & B c= A +^ B )
proof
let A, B be Ordinal; ::_thesis: ( A c= A +^ B & B c= A +^ B )
A1: {} +^ B c= A +^ B by ORDINAL2:34, XBOOLE_1:2;
 A +^ {} c= A +^ B by ORDINAL2:33, XBOOLE_1:2;
hence  ( A c= A +^ B & B c= A +^ B ) by A1, ORDINAL2:27, ORDINAL2:30; ::_thesis: verum
end;

theorem :: ORDINAL3:25
for A, B, C being Ordinal st A in B holds
( A in B +^ C & A in C +^ B )
proof
let A, B, C be Ordinal; ::_thesis: ( A in B implies ( A in B +^ C & A in C +^ B ) )
assume A1: A in B ; ::_thesis: ( A in B +^ C & A in C +^ B )
A2: B c= C +^ B by Th24;
 B c= B +^ C by Th24;
hence  ( A in B +^ C & A in C +^ B ) by A1, A2; ::_thesis: verum
end;

theorem Th26: :: ORDINAL3:26
for A, B being Ordinal st A +^ B = {} holds
( A = {} & B = {} )
proof
let A, B be Ordinal; ::_thesis: ( A +^ B = {} implies ( A = {} & B = {} ) )
assume A1: A +^ B = {} ; ::_thesis: ( A = {} & B = {} )
then A2: B c= {} by Th24;
 A c= {} by A1, Th24;
hence  ( A = {} & B = {} ) by A2, XBOOLE_1:3; ::_thesis: verum
end;

theorem Th27: :: ORDINAL3:27
for A, B being Ordinal st A c= B holds
ex C being Ordinal st B = A +^ C
proof
let A, B be Ordinal; ::_thesis: ( A c= B implies ex C being Ordinal st B = A +^ C )
defpred S1[ Ordinal] means ( A c= $1 implies ex C being Ordinal st $1 = A +^ C );
A1: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume that
A2: ( A c= B implies ex C being Ordinal st B = A +^ C ) and
A3: A c= succ B ; ::_thesis: ex C being Ordinal st succ B = A +^ C
A4: now__::_thesis:_(_A_<>_succ_B_implies_ex_C_being_Ordinal_st_succ_B_=_A_+^_C_)
assume  A <> succ B ; ::_thesis: ex C being Ordinal st succ B = A +^ C
then  A c< succ B by A3, XBOOLE_0:def_8;
then  A in succ B by ORDINAL1:11;
then consider C being Ordinal such that
A5: B = A +^ C by A2, ORDINAL1:22;
 succ B = A +^ (succ C) by A5, ORDINAL2:28;
hence  ex C being Ordinal st succ B = A +^ C ; ::_thesis: verum
end;
 ( A = succ B implies succ B = A +^ {} ) by ORDINAL2:27;
hence  ex C being Ordinal st succ B = A +^ C by A4; ::_thesis: verum
end;
A6: for B being Ordinal st B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) holds
S1[B]
proof
deffunc H1( Ordinal) ->  set = A +^ $1;
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume that
 B <> {} and
A7: B is limit_ordinal and
 for C being Ordinal st C in B & A c= C holds
ex D being Ordinal st C = A +^ D and
A8: A c= B ; ::_thesis: ex C being Ordinal st B = A +^ C
defpred S2[ Ordinal] means B c= A +^ $1;
A9: B = {} +^ B by ORDINAL2:30;
 {} +^ B c= A +^ B by ORDINAL2:34, XBOOLE_1:2;
then A10: ex C being Ordinal st S2[C] by A9;
consider C being Ordinal such that
A11: ( S2[C] & ( for D being Ordinal st S2[D] holds
C c= D ) ) from ORDINAL1:sch_1(A10);
consider L being Ordinal-Sequence such that
A12: ( dom L = C & ( for D being Ordinal st D in C holds
L . D = H1(D) ) ) from ORDINAL2:sch_3();
A13: now__::_thesis:_(_C_<>_{}_implies_ex_C_being_Ordinal_st_B_=_A_+^_C_)
 for D being Ordinal st D in rng L holds
D in B
proof
let D be Ordinal; ::_thesis: ( D in rng L implies D in B )
assume  D in rng L ; ::_thesis: D in B
then consider y being set  such that
A14: y in dom L and
A15: D = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A14;
A16: not C c= y by A12, A14, ORDINAL1:5;
 L . y = A +^ y by A12, A14;
hence  D in B by A11, A15, A16, ORDINAL1:16; ::_thesis: verum
end;
then A17: sup (rng L) c= B by ORDINAL2:20;
A18: C is limit_ordinal
proof
assume  not C is limit_ordinal ; ::_thesis: contradiction
then consider D being Ordinal such that
A19: C = succ D by ORDINAL1:29;
 not C c= D by A19, ORDINAL1:5, ORDINAL1:6;
then  A +^ D in B by A11, ORDINAL1:16;
then A20: succ (A +^ D) c= B by ORDINAL1:21;
 succ (A +^ D) = A +^ (succ D) by ORDINAL2:28;
then  B = succ (A +^ D) by A11, A19, A20, XBOOLE_0:def_10;
hence  contradiction by A7, ORDINAL1:29; ::_thesis: verum
end;
assume  C <> {} ; ::_thesis: ex C being Ordinal st B = A +^ C
then A +^ C = sup L by A12, A18, ORDINAL2:29
.= sup (rng L) ;
then  B = A +^ C by A11, A17, XBOOLE_0:def_10;
hence  ex C being Ordinal st B = A +^ C ; ::_thesis: verum
end;
now__::_thesis:_(_C_=_{}_implies_B_=_A_+^_{}_)
assume  C = {} ; ::_thesis: B = A +^ {}
then  A +^ C = A by ORDINAL2:27;
hence B = A by A8, A11, XBOOLE_0:def_10
.= A +^ {} by ORDINAL2:27 ;
::_thesis: verum
end;
hence  ex C being Ordinal st B = A +^ C by A13; ::_thesis: verum
end;
A21: S1[ {} ]
proof
assume  A c= {} ; ::_thesis: ex C being Ordinal st {} = A +^ C
then  A = {} by XBOOLE_1:3;
then  {} = A +^ {} by ORDINAL2:30;
hence  ex C being Ordinal st {} = A +^ C ; ::_thesis: verum
end;
 for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A21, A1, A6);
hence  ( A c= B implies ex C being Ordinal st B = A +^ C ) ; ::_thesis: verum
end;

theorem Th28: :: ORDINAL3:28
for A, B being Ordinal st A in B holds
ex C being Ordinal st
( B = A +^ C & C <> {} )
proof
let A, B be Ordinal; ::_thesis: ( A in B implies ex C being Ordinal st
( B = A +^ C & C <> {} ) )
assume A1: A in B ; ::_thesis: ex C being Ordinal st
( B = A +^ C & C <> {} )
then  A c= B by ORDINAL1:def_2;
then consider C being Ordinal such that
A2: B = A +^ C by Th27;
take  C ; ::_thesis: ( B = A +^ C & C <> {} )
thus  B = A +^ C by A2; ::_thesis: C <> {}
assume  C = {} ; ::_thesis: contradiction
then  B = A by A2, ORDINAL2:27;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th29: :: ORDINAL3:29
for A, B being Ordinal st A <> {} & A is limit_ordinal holds
B +^ A is limit_ordinal
proof
let A, B be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal implies B +^ A is limit_ordinal )
assume that
A1: A <> {} and
A2: A is limit_ordinal ; ::_thesis: B +^ A is limit_ordinal
 {} c= A by XBOOLE_1:2;
then A3: {} c< A by A1, XBOOLE_0:def_8;
deffunc H1( Ordinal) ->  set = B +^ $1;
consider L being Ordinal-Sequence such that
A4: ( dom L = A & ( for C being Ordinal st C in A holds
L . C = H1(C) ) ) from ORDINAL2:sch_3();
A5: B +^ A = sup L by A1, A2, A4, ORDINAL2:29
.= sup (rng L) ;
 for C being Ordinal st C in B +^ A holds
succ C in B +^ A
proof
let C be Ordinal; ::_thesis: ( C in B +^ A implies succ C in B +^ A )
assume A6: C in B +^ A ; ::_thesis: succ C in B +^ A
A7: now__::_thesis:_(_not_C_in_B_implies_succ_C_in_B_+^_A_)
assume  not C in B ; ::_thesis: succ C in B +^ A
then consider D being Ordinal such that
A8: C = B +^ D by Th27, ORDINAL1:16;
now__::_thesis:_D_in_A
assume  not D in A ; ::_thesis: contradiction
then  B +^ A c= B +^ D by ORDINAL1:16, ORDINAL2:33;
then  C in C by A6, A8;
hence  contradiction ; ::_thesis: verum
end;
then A9: succ D in A by A2, ORDINAL1:28;
then L . (succ D) = B +^ (succ D) by A4
.= succ (B +^ D) by ORDINAL2:28 ;
then  succ C in rng L by A4, A8, A9, FUNCT_1:def_3;
hence  succ C in B +^ A by A5, ORDINAL2:19; ::_thesis: verum
end;
now__::_thesis:_(_C_in_B_implies_succ_C_in_B_+^_A_)
assume  C in B ; ::_thesis: succ C in B +^ A
then A10: succ C c= B by ORDINAL1:21;
A11: (succ C) +^ {} = succ C by ORDINAL2:27;
 B +^ {} in B +^ A by A3, ORDINAL1:11, ORDINAL2:32;
hence  succ C in B +^ A by A10, A11, ORDINAL1:12, ORDINAL2:34; ::_thesis: verum
end;
hence  succ C in B +^ A by A7; ::_thesis: verum
end;
hence  B +^ A is limit_ordinal by ORDINAL1:28; ::_thesis: verum
end;

theorem Th30: :: ORDINAL3:30
for A, B, C being Ordinal holds (A +^ B) +^ C = A +^ (B +^ C)
proof
let A, B, C be Ordinal; ::_thesis: (A +^ B) +^ C = A +^ (B +^ C)
defpred S1[ Ordinal] means (A +^ B) +^ $1 = A +^ (B +^ $1);
A1: for C being Ordinal st S1[C] holds
S1[ succ C]
proof
let C be Ordinal; ::_thesis: ( S1[C] implies S1[ succ C] )
assume A2: (A +^ B) +^ C = A +^ (B +^ C) ; ::_thesis: S1[ succ C]
thus (A +^ B) +^ (succ C) = succ ((A +^ B) +^ C) by ORDINAL2:28
.= A +^ (succ (B +^ C)) by A2, ORDINAL2:28
.= A +^ (B +^ (succ C)) by ORDINAL2:28 ; ::_thesis: verum
end;
A3: for C being Ordinal st C <> {} & C is limit_ordinal & ( for D being Ordinal st D in C holds
S1[D] ) holds
S1[C]
proof
deffunc H1( Ordinal) ->  set = (A +^ B) +^ $1;
let C be Ordinal; ::_thesis: ( C <> {} & C is limit_ordinal & ( for D being Ordinal st D in C holds
S1[D] ) implies S1[C] )
assume that
A4: C <> {} and
A5: C is limit_ordinal and
A6: for D being Ordinal st D in C holds
S1[D] ; ::_thesis: S1[C]
consider L being Ordinal-Sequence such that
A7: ( dom L = C & ( for D being Ordinal st D in C holds
L . D = H1(D) ) ) from ORDINAL2:sch_3();
deffunc H2( Ordinal) ->  set = A +^ $1;
consider L1 being Ordinal-Sequence such that
A8: ( dom L1 = B +^ C & ( for D being Ordinal st D in B +^ C holds
L1 . D = H2(D) ) ) from ORDINAL2:sch_3();
A9: rng L c= rng L1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng L or x in rng L1 )
assume  x in rng L ; ::_thesis: x in rng L1
then consider y being set  such that
A10: y in dom L and
A11: x = L . y by FUNCT_1:def_3;
reconsider y = y as Ordinal by A10;
A12: B +^ y in B +^ C by A7, A10, ORDINAL2:32;
 L . y = (A +^ B) +^ y by A7, A10;
then A13: L . y = A +^ (B +^ y) by A6, A7, A10;
 L1 . (B +^ y) = A +^ (B +^ y) by A7, A8, A10, ORDINAL2:32;
hence  x in rng L1 by A8, A11, A13, A12, FUNCT_1:def_3; ::_thesis: verum
end;
A14: B +^ C <> {} by A4, Th26;
 B +^ C is limit_ordinal by A4, A5, Th29;
then A15: A +^ (B +^ C) = sup L1 by A8, A14, ORDINAL2:29
.= sup (rng L1) ;
(A +^ B) +^ C = sup L by A4, A5, A7, ORDINAL2:29
.= sup (rng L) ;
hence  (A +^ B) +^ C c= A +^ (B +^ C) by A15, A9, ORDINAL2:22; :: according to XBOOLE_0:def_10 ::_thesis: A +^ (B +^ C) c= (A +^ B) +^ C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A +^ (B +^ C) or x in (A +^ B) +^ C )
assume A16: x in A +^ (B +^ C) ; ::_thesis: x in (A +^ B) +^ C
then reconsider x9 = x as Ordinal ;
A17: now__::_thesis:_(_not_x_in_A_+^_B_implies_x_in_(A_+^_B)_+^_C_)
A18: A c= A +^ B by Th24;
assume A19: not x in A +^ B ; ::_thesis: x in (A +^ B) +^ C
then  A +^ B c= x9 by ORDINAL1:16;
then consider E being Ordinal such that
A20: x9 = A +^ E by A18, Th27, XBOOLE_1:1;
 B c= E by A19, A20, ORDINAL1:16, ORDINAL2:32;
then consider F being Ordinal such that
A21: E = B +^ F by Th27;
A22: now__::_thesis:_F_in_C
assume  not F in C ; ::_thesis: contradiction
then  B +^ C c= B +^ F by ORDINAL1:16, ORDINAL2:33;
then  A +^ (B +^ C) c= A +^ (B +^ F) by ORDINAL2:33;
then  x9 in x9 by A16, A20, A21;
hence  contradiction ; ::_thesis: verum
end;
then  x = (A +^ B) +^ F by A6, A20, A21;
hence  x in (A +^ B) +^ C by A22, ORDINAL2:32; ::_thesis: verum
end;
A23: (A +^ B) +^ {} = A +^ B by ORDINAL2:27;
 (A +^ B) +^ {} c= (A +^ B) +^ C by ORDINAL2:33, XBOOLE_1:2;
hence  x in (A +^ B) +^ C by A23, A17; ::_thesis: verum
end;
(A +^ B) +^ {} = A +^ B by ORDINAL2:27
.= A +^ (B +^ {}) by ORDINAL2:27 ;
then A24: S1[ {} ] ;
 for C being Ordinal holds S1[C] from ORDINAL2:sch_1(A24, A1, A3);
hence  (A +^ B) +^ C = A +^ (B +^ C) ; ::_thesis: verum
end;

theorem :: ORDINAL3:31
for A, B being Ordinal holds
( not A *^ B = {} or A = {} or B = {} )
proof
let A, B be Ordinal; ::_thesis: ( not A *^ B = {} or A = {} or B = {} )
assume that
A1: A *^ B = {} and
A2: A <> {} and
A3: B <> {} ; ::_thesis: contradiction
 {} c= A by XBOOLE_1:2;
then  {} c< A by A2, XBOOLE_0:def_8;
hence  contradiction by A1, A3, ORDINAL1:11, ORDINAL2:40; ::_thesis: verum
end;

theorem :: ORDINAL3:32
for A, B, C being Ordinal st A in B & C <> {} holds
( A in B *^ C & A in C *^ B )
proof
let A, B, C be Ordinal; ::_thesis: ( A in B & C <> {} implies ( A in B *^ C & A in C *^ B ) )
assume that
A1: A in B and
A2: C <> {} ; ::_thesis: ( A in B *^ C & A in C *^ B )
 {} c= C by XBOOLE_1:2;
then  {} c< C by A2, XBOOLE_0:def_8;
then  {} in C by ORDINAL1:11;
then A3: 1 c= C by Lm1, ORDINAL1:21;
then A4: 1 *^ B c= C *^ B by ORDINAL2:41;
A5: 1 *^ B = B by ORDINAL2:39;
A6: B *^ 1 = B by ORDINAL2:39;
 B *^ 1 c= B *^ C by A3, ORDINAL2:42;
hence  ( A in B *^ C & A in C *^ B ) by A1, A4, A6, A5; ::_thesis: verum
end;

theorem Th33: :: ORDINAL3:33
for B, A, C being Ordinal st B *^ A = C *^ A & A <> {} holds
B = C
proof
let B, A, C be Ordinal; ::_thesis: ( B *^ A = C *^ A & A <> {} implies B = C )
assume that
A1: B *^ A = C *^ A and
A2: A <> {} and
A3: B <> C ; ::_thesis: contradiction
 ( B in C or C in B ) by A3, ORDINAL1:14;
then  B *^ A in B *^ A by A1, A2, ORDINAL2:40;
hence  contradiction ; ::_thesis: verum
end;

theorem Th34: :: ORDINAL3:34
for B, A, C being Ordinal st B *^ A in C *^ A holds
B in C
proof
let B, A, C be Ordinal; ::_thesis: ( B *^ A in C *^ A implies B in C )
assume that
A1: B *^ A in C *^ A and
A2: not B in C ; ::_thesis: contradiction
 C c= B by A2, ORDINAL1:16;
hence  contradiction by A1, ORDINAL1:5, ORDINAL2:41; ::_thesis: verum
end;

theorem Th35: :: ORDINAL3:35
for B, A, C being Ordinal st B *^ A c= C *^ A & A <> {} holds
B c= C
proof
let B, A, C be Ordinal; ::_thesis: ( B *^ A c= C *^ A & A <> {} implies B c= C )
assume A1: B *^ A c= C *^ A ; ::_thesis: ( not A <> {} or B c= C )
 ( ( B *^ A c= C *^ A & B *^ A <> C *^ A ) iff B *^ A c< C *^ A ) by XBOOLE_0:def_8;
then  not ( A <> {} & not B = C & not B in C ) by A1, Th33, Th34, ORDINAL1:11;
hence  ( not A <> {} or B c= C ) by ORDINAL1:def_2; ::_thesis: verum
end;

theorem Th36: :: ORDINAL3:36
for B, A being Ordinal st B <> {} holds
( A c= A *^ B & A c= B *^ A )
proof
let B, A be Ordinal; ::_thesis: ( B <> {} implies ( A c= A *^ B & A c= B *^ A ) )
assume  B <> {} ; ::_thesis: ( A c= A *^ B & A c= B *^ A )
then  {} in B by Th8;
then A1: 1 c= B by Lm1, ORDINAL1:21;
then A2: A *^ 1 c= A *^ B by ORDINAL2:42;
 1 *^ A c= B *^ A by A1, ORDINAL2:41;
hence  ( A c= A *^ B & A c= B *^ A ) by A2, ORDINAL2:39; ::_thesis: verum
end;

theorem :: ORDINAL3:37
for A, B being Ordinal st A *^ B = 1 holds
( A = 1 & B = 1 )
proof
let A, B be Ordinal; ::_thesis: ( A *^ B = 1 implies ( A = 1 & B = 1 ) )
assume A1: A *^ B = 1 ; ::_thesis: ( A = 1 & B = 1 )
then A2: B <> {} by ORDINAL2:38;
 {} c= B by XBOOLE_1:2;
then  {} c< B by A2, XBOOLE_0:def_8;
then  {} in B by ORDINAL1:11;
then A3: 1 c= B by Lm1, ORDINAL1:21;
A4: now__::_thesis:_not_1_in_A
A5: B = 1 *^ B by ORDINAL2:39;
assume  1 in A ; ::_thesis: contradiction
hence  contradiction by A1, A2, A3, A5, ORDINAL1:5, ORDINAL2:40; ::_thesis: verum
end;
now__::_thesis:_not_A_in_1
assume  A in 1 ; ::_thesis: contradiction
then  A c= {} by Lm1, ORDINAL1:22;
then  A = {} by XBOOLE_1:3;
hence  contradiction by A1, ORDINAL2:35; ::_thesis: verum
end;
hence  A = 1 by A4, ORDINAL1:14; ::_thesis: B = 1
hence  B = 1 by A1, ORDINAL2:39; ::_thesis: verum
end;

theorem Th38: :: ORDINAL3:38
for A, B, C being Ordinal holds
( not A in B +^ C or A in B or ex D being Ordinal st
( D in C & A = B +^ D ) )
proof
let A, B, C be Ordinal; ::_thesis: ( not A in B +^ C or A in B or ex D being Ordinal st
( D in C & A = B +^ D ) )
assume that
A1: A in B +^ C and
A2: not A in B ; ::_thesis: ex D being Ordinal st
( D in C & A = B +^ D )
consider D being Ordinal such that
A3: A = B +^ D by A2, Th27, ORDINAL1:16;
take  D ; ::_thesis: ( D in C & A = B +^ D )
assume  ( not D in C or not A = B +^ D ) ; ::_thesis: contradiction
then  C c= D by A3, ORDINAL1:16;
hence  contradiction by A1, A3, ORDINAL1:5, ORDINAL2:33; ::_thesis: verum
end;

definition
let C be Ordinal;
let fi be Ordinal-Sequence;
funcC +^ fi ->  Ordinal-Sequence means :Def1: :: ORDINAL3:def 1
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = C +^ (fi . A) ) );
existence
 ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C +^ (fi . A) ) )
proof
deffunc H1( Ordinal) ->  set = C +^ (fi . $1);
thus  ex F being Ordinal-Sequence st
( dom F = dom fi & ( for A being Ordinal st A in dom fi holds
F . A = H1(A) ) ) from ORDINAL2:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C +^ (fi . A) ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = C +^ (fi . A) ) holds
b1 = b2
proof
let f1, f2 be Ordinal-Sequence; ::_thesis: ( dom f1 = dom fi & ( for A being Ordinal st A in dom fi holds
f1 . A = C +^ (fi . A) ) & dom f2 = dom fi & ( for A being Ordinal st A in dom fi holds
f2 . A = C +^ (fi . A) ) implies f1 = f2 )
assume that
A1: dom f1 = dom fi and
A2: for A being Ordinal st A in dom fi holds
f1 . A = C +^ (fi . A) and
A3: dom f2 = dom fi and
A4: for A being Ordinal st A in dom fi holds
f2 . A = C +^ (fi . A) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_fi_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom fi implies f1 . x = f2 . x )
assume A5: x in dom fi ; ::_thesis: f1 . x = f2 . x
then reconsider A = x as Ordinal ;
thus f1 . x = C +^ (fi . A) by A2, A5
.= f2 . x by A4, A5 ; ::_thesis: verum
end;
hence  f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
funcfi +^ C ->  Ordinal-Sequence means :: ORDINAL3:def 2
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = (fi . A) +^ C ) );
existence
 ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) +^ C ) )
proof
deffunc H1( Ordinal) ->  set = (fi . $1) +^ C;
thus  ex F being Ordinal-Sequence st
( dom F = dom fi & ( for A being Ordinal st A in dom fi holds
F . A = H1(A) ) ) from ORDINAL2:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) +^ C ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = (fi . A) +^ C ) holds
b1 = b2
proof
let f1, f2 be Ordinal-Sequence; ::_thesis: ( dom f1 = dom fi & ( for A being Ordinal st A in dom fi holds
f1 . A = (fi . A) +^ C ) & dom f2 = dom fi & ( for A being Ordinal st A in dom fi holds
f2 . A = (fi . A) +^ C ) implies f1 = f2 )
assume that
A6: dom f1 = dom fi and
A7: for A being Ordinal st A in dom fi holds
f1 . A = (fi . A) +^ C and
A8: dom f2 = dom fi and
A9: for A being Ordinal st A in dom fi holds
f2 . A = (fi . A) +^ C ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_fi_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom fi implies f1 . x = f2 . x )
assume A10: x in dom fi ; ::_thesis: f1 . x = f2 . x
then reconsider A = x as Ordinal ;
thus f1 . x = (fi . A) +^ C by A7, A10
.= f2 . x by A9, A10 ; ::_thesis: verum
end;
hence  f1 = f2 by A6, A8, FUNCT_1:2; ::_thesis: verum
end;
funcC *^ fi ->  Ordinal-Sequence means :: ORDINAL3:def 3
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = C *^ (fi . A) ) );
existence
 ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C *^ (fi . A) ) )
proof
deffunc H1( Ordinal) ->  set = C *^ (fi . $1);
thus  ex F being Ordinal-Sequence st
( dom F = dom fi & ( for A being Ordinal st A in dom fi holds
F . A = H1(A) ) ) from ORDINAL2:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = C *^ (fi . A) ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = C *^ (fi . A) ) holds
b1 = b2
proof
let f1, f2 be Ordinal-Sequence; ::_thesis: ( dom f1 = dom fi & ( for A being Ordinal st A in dom fi holds
f1 . A = C *^ (fi . A) ) & dom f2 = dom fi & ( for A being Ordinal st A in dom fi holds
f2 . A = C *^ (fi . A) ) implies f1 = f2 )
assume that
A11: dom f1 = dom fi and
A12: for A being Ordinal st A in dom fi holds
f1 . A = C *^ (fi . A) and
A13: dom f2 = dom fi and
A14: for A being Ordinal st A in dom fi holds
f2 . A = C *^ (fi . A) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_fi_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom fi implies f1 . x = f2 . x )
assume A15: x in dom fi ; ::_thesis: f1 . x = f2 . x
then reconsider A = x as Ordinal ;
thus f1 . x = C *^ (fi . A) by A12, A15
.= f2 . x by A14, A15 ; ::_thesis: verum
end;
hence  f1 = f2 by A11, A13, FUNCT_1:2; ::_thesis: verum
end;
funcfi *^ C ->  Ordinal-Sequence means :Def4: :: ORDINAL3:def 4
( dom it = dom fi & ( for A being Ordinal st A in dom fi holds
it . A = (fi . A) *^ C ) );
existence
 ex b1 being Ordinal-Sequence st
( dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) *^ C ) )
proof
deffunc H1( Ordinal) ->  set = (fi . $1) *^ C;
thus  ex F being Ordinal-Sequence st
( dom F = dom fi & ( for A being Ordinal st A in dom fi holds
F . A = H1(A) ) ) from ORDINAL2:sch_3(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal-Sequence st dom b1 = dom fi & ( for A being Ordinal st A in dom fi holds
b1 . A = (fi . A) *^ C ) & dom b2 = dom fi & ( for A being Ordinal st A in dom fi holds
b2 . A = (fi . A) *^ C ) holds
b1 = b2
proof
let f1, f2 be Ordinal-Sequence; ::_thesis: ( dom f1 = dom fi & ( for A being Ordinal st A in dom fi holds
f1 . A = (fi . A) *^ C ) & dom f2 = dom fi & ( for A being Ordinal st A in dom fi holds
f2 . A = (fi . A) *^ C ) implies f1 = f2 )
assume that
A16: dom f1 = dom fi and
A17: for A being Ordinal st A in dom fi holds
f1 . A = (fi . A) *^ C and
A18: dom f2 = dom fi and
A19: for A being Ordinal st A in dom fi holds
f2 . A = (fi . A) *^ C ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_fi_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom fi implies f1 . x = f2 . x )
assume A20: x in dom fi ; ::_thesis: f1 . x = f2 . x
then reconsider A = x as Ordinal ;
thus f1 . x = (fi . A) *^ C by A17, A20
.= f2 . x by A19, A20 ; ::_thesis: verum
end;
hence  f1 = f2 by A16, A18, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines +^ ORDINAL3:def_1_:_
 for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = C +^ fi iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = C +^ (fi . A) ) ) );

:: deftheorem  defines +^ ORDINAL3:def_2_:_
 for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = fi +^ C iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = (fi . A) +^ C ) ) );

:: deftheorem  defines *^ ORDINAL3:def_3_:_
 for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = C *^ fi iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = C *^ (fi . A) ) ) );

:: deftheorem Def4 defines *^ ORDINAL3:def_4_:_
 for C being Ordinal
for fi, b3 being Ordinal-Sequence holds
( b3 = fi *^ C iff ( dom b3 = dom fi & ( for A being Ordinal st A in dom fi holds
b3 . A = (fi . A) *^ C ) ) );

theorem Th39: :: ORDINAL3:39
for fi, psi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ) holds
sup psi = C +^ (sup fi)
proof
let fi, psi be Ordinal-Sequence; ::_thesis: for C being Ordinal st {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ) holds
sup psi = C +^ (sup fi)
let C be Ordinal; ::_thesis: ( {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ) implies sup psi = C +^ (sup fi) )
assume that
A1: {} <> dom fi and
A2: dom fi = dom psi and
A3: for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ; ::_thesis: sup psi = C +^ (sup fi)
set z = the Element of dom fi;
reconsider z9 = fi . the Element of dom fi as Ordinal ;
A4: C +^ (sup (rng fi)) c= sup (rng psi)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C +^ (sup (rng fi)) or x in sup (rng psi) )
assume A5: x in C +^ (sup (rng fi)) ; ::_thesis: x in sup (rng psi)
then reconsider A = x as Ordinal ;
A6: now__::_thesis:_(_ex_B_being_Ordinal_st_
(_B_in_sup_(rng_fi)_&_A_=_C_+^_B_)_implies_A_in_sup_(rng_psi)_)
given B being Ordinal such that A7: B in sup (rng fi) and
A8: A = C +^ B ; ::_thesis: A in sup (rng psi)
consider D being Ordinal such that
A9: D in rng fi and
A10: B c= D by A7, ORDINAL2:21;
consider x being set  such that
A11: x in dom fi and
A12: D = fi . x by A9, FUNCT_1:def_3;
reconsider x = x as Ordinal by A11;
 psi . x = C +^ D by A3, A11, A12;
then  C +^ D in rng psi by A2, A11, FUNCT_1:def_3;
then  C +^ D in sup (rng psi) by ORDINAL2:19;
hence  A in sup (rng psi) by A8, A10, ORDINAL1:12, ORDINAL2:33; ::_thesis: verum
end;
now__::_thesis:_(_A_in_C_implies_A_in_sup_(rng_psi)_)
 C +^ z9 = psi . the Element of dom fi by A1, A3;
then  C +^ z9 in rng psi by A1, A2, FUNCT_1:def_3;
then A13: C +^ z9 in sup (rng psi) by ORDINAL2:19;
assume A14: A in C ; ::_thesis: A in sup (rng psi)
 C c= C +^ z9 by Th24;
then  A c= C +^ z9 by A14, ORDINAL1:def_2;
hence  A in sup (rng psi) by A13, ORDINAL1:12; ::_thesis: verum
end;
hence  x in sup (rng psi) by A5, A6, Th38; ::_thesis: verum
end;
 sup (rng psi) c= C +^ (sup (rng fi))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sup (rng psi) or x in C +^ (sup (rng fi)) )
assume A15: x in sup (rng psi) ; ::_thesis: x in C +^ (sup (rng fi))
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A16: B in rng psi and
A17: A c= B by A15, ORDINAL2:21;
consider y being set  such that
A18: y in dom psi and
A19: B = psi . y by A16, FUNCT_1:def_3;
reconsider y = y as Ordinal by A18;
reconsider y9 = fi . y as Ordinal ;
 y9 in rng fi by A2, A18, FUNCT_1:def_3;
then A20: y9 in sup (rng fi) by ORDINAL2:19;
 B = C +^ y9 by A2, A3, A18, A19;
then  B in C +^ (sup (rng fi)) by A20, ORDINAL2:32;
hence  x in C +^ (sup (rng fi)) by A17, ORDINAL1:12; ::_thesis: verum
end;
hence  sup psi = C +^ (sup fi) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th40: :: ORDINAL3:40
for A, B being Ordinal st A is limit_ordinal holds
A *^ B is limit_ordinal
proof
let A, B be Ordinal; ::_thesis: ( A is limit_ordinal implies A *^ B is limit_ordinal )
A1: now__::_thesis:_(_A_<>_{}_&_A_is_limit_ordinal_&_A_is_limit_ordinal_implies_A_*^_B_is_limit_ordinal_)
deffunc H1( Ordinal) ->  set = $1 *^ B;
assume that
A2: A <> {} and
A3: A is limit_ordinal ; ::_thesis: ( A is limit_ordinal implies A *^ B is limit_ordinal )
consider fi being Ordinal-Sequence such that
A4: ( dom fi = A & ( for C being Ordinal st C in A holds
fi . C = H1(C) ) ) from ORDINAL2:sch_3();
A5: A *^ B = union (sup fi) by A2, A3, A4, ORDINAL2:37
.= union (sup (rng fi)) ;
 for C being Ordinal st C in A *^ B holds
succ C in A *^ B
proof
let C be Ordinal; ::_thesis: ( C in A *^ B implies succ C in A *^ B )
assume A6: C in A *^ B ; ::_thesis: succ C in A *^ B
then consider X being set  such that
A7: C in X and
A8: X in sup (rng fi) by A5, TARSKI:def_4;
reconsider X = X as Ordinal by A8;
consider D being Ordinal such that
A9: D in rng fi and
A10: X c= D by A8, ORDINAL2:21;
consider x being set  such that
A11: x in dom fi and
A12: D = fi . x by A9, FUNCT_1:def_3;
 succ C c= D by A7, A10, ORDINAL1:21;
then A13: succ C in succ D by ORDINAL1:22;
reconsider x = x as Ordinal by A11;
A14: succ x in dom fi by A3, A4, A11, ORDINAL1:28;
then fi . (succ x) = (succ x) *^ B by A4
.= (x *^ B) +^ B by ORDINAL2:36 ;
then  (x *^ B) +^ B in rng fi by A14, FUNCT_1:def_3;
then A15: (x *^ B) +^ B in sup (rng fi) by ORDINAL2:19;
A16: (x *^ B) +^ (succ {}) = succ ((x *^ B) +^ {}) by ORDINAL2:28;
 B <> {} by A6, ORDINAL2:38;
then  {} in B by Th8;
then A17: succ {} c= B by ORDINAL1:21;
A18: (x *^ B) +^ {} = x *^ B by ORDINAL2:27;
 x *^ B = fi . x by A4, A11;
then  succ D in sup (rng fi) by A12, A17, A16, A18, A15, ORDINAL1:12, ORDINAL2:33;
hence  succ C in A *^ B by A5, A13, TARSKI:def_4; ::_thesis: verum
end;
hence  ( A is limit_ordinal implies A *^ B is limit_ordinal ) by ORDINAL1:28; ::_thesis: verum
end;
assume  A is limit_ordinal ; ::_thesis: A *^ B is limit_ordinal
hence  A *^ B is limit_ordinal by A1, ORDINAL2:35; ::_thesis: verum
end;

theorem Th41: :: ORDINAL3:41
for A, B, C being Ordinal st A in B *^ C & B is limit_ordinal holds
ex D being Ordinal st
( D in B & A in D *^ C )
proof
let A, B, C be Ordinal; ::_thesis: ( A in B *^ C & B is limit_ordinal implies ex D being Ordinal st
( D in B & A in D *^ C ) )
assume that
A1: A in B *^ C and
A2: B is limit_ordinal ; ::_thesis: ex D being Ordinal st
( D in B & A in D *^ C )
deffunc H1( Ordinal) ->  set = $1 *^ C;
consider fi being Ordinal-Sequence such that
A3: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
 B <> {} by A1, ORDINAL2:35;
then B *^ C = union (sup fi) by A2, A3, ORDINAL2:37
.= union (sup (rng fi)) ;
then consider X being set  such that
A4: A in X and
A5: X in sup (rng fi) by A1, TARSKI:def_4;
reconsider X = X as Ordinal by A5;
consider D being Ordinal such that
A6: D in rng fi and
A7: X c= D by A5, ORDINAL2:21;
consider x being set  such that
A8: x in dom fi and
A9: D = fi . x by A6, FUNCT_1:def_3;
reconsider x = x as Ordinal by A8;
take E = succ x; ::_thesis: ( E in B & A in E *^ C )
thus  E in B by A2, A3, A8, ORDINAL1:28; ::_thesis: A in E *^ C
A10: D +^ {} = D by ORDINAL2:27;
A11: C <> {} by A1, ORDINAL2:38;
E *^ C = (x *^ C) +^ C by ORDINAL2:36
.= D +^ C by A3, A8, A9 ;
then  D in E *^ C by A11, A10, Th8, ORDINAL2:32;
hence  A in E *^ C by A4, A7, ORDINAL1:10; ::_thesis: verum
end;

theorem Th42: :: ORDINAL3:42
for fi, psi being Ordinal-Sequence
for C being Ordinal st dom fi = dom psi & C <> {} & sup fi is limit_ordinal & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = B *^ C ) holds
sup psi = (sup fi) *^ C
proof
let fi, psi be Ordinal-Sequence; ::_thesis: for C being Ordinal st dom fi = dom psi & C <> {} & sup fi is limit_ordinal & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = B *^ C ) holds
sup psi = (sup fi) *^ C
let C be Ordinal; ::_thesis: ( dom fi = dom psi & C <> {} & sup fi is limit_ordinal & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = B *^ C ) implies sup psi = (sup fi) *^ C )
assume that
A1: dom fi = dom psi and
A2: C <> {} and
A3: sup fi is limit_ordinal and
A4: for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = B *^ C ; ::_thesis: sup psi = (sup fi) *^ C
A5: (sup (rng fi)) *^ C c= sup (rng psi)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (sup (rng fi)) *^ C or x in sup (rng psi) )
assume A6: x in (sup (rng fi)) *^ C ; ::_thesis: x in sup (rng psi)
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A7: B in sup (rng fi) and
A8: A in B *^ C by A3, A6, Th41;
consider D being Ordinal such that
A9: D in rng fi and
A10: B c= D by A7, ORDINAL2:21;
consider y being set  such that
A11: y in dom fi and
A12: D = fi . y by A9, FUNCT_1:def_3;
reconsider y = y as Ordinal by A11;
reconsider y9 = psi . y as Ordinal ;
A13: y9 in rng psi by A1, A11, FUNCT_1:def_3;
 y9 = D *^ C by A4, A11, A12;
then A14: D *^ C in sup (rng psi) by A13, ORDINAL2:19;
 B *^ C c= D *^ C by A10, ORDINAL2:41;
hence  x in sup (rng psi) by A8, A14, ORDINAL1:10; ::_thesis: verum
end;
 sup (rng psi) c= (sup (rng fi)) *^ C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sup (rng psi) or x in (sup (rng fi)) *^ C )
assume A15: x in sup (rng psi) ; ::_thesis: x in (sup (rng fi)) *^ C
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A16: B in rng psi and
A17: A c= B by A15, ORDINAL2:21;
consider y being set  such that
A18: y in dom psi and
A19: B = psi . y by A16, FUNCT_1:def_3;
reconsider y = y as Ordinal by A18;
reconsider y9 = fi . y as Ordinal ;
 y9 in rng fi by A1, A18, FUNCT_1:def_3;
then A20: y9 in sup (rng fi) by ORDINAL2:19;
 B = y9 *^ C by A1, A4, A18, A19;
then  B in (sup (rng fi)) *^ C by A2, A20, ORDINAL2:40;
hence  x in (sup (rng fi)) *^ C by A17, ORDINAL1:12; ::_thesis: verum
end;
hence  sup psi = (sup fi) *^ C by A5, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th43: :: ORDINAL3:43
for fi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi holds
sup (C +^ fi) = C +^ (sup fi)
proof
let fi be Ordinal-Sequence; ::_thesis: for C being Ordinal st {} <> dom fi holds
sup (C +^ fi) = C +^ (sup fi)
let C be Ordinal; ::_thesis: ( {} <> dom fi implies sup (C +^ fi) = C +^ (sup fi) )
A1: for A, B being Ordinal st A in dom fi & B = fi . A holds
(C +^ fi) . A = C +^ B by Def1;
 dom (C +^ fi) = dom fi by Def1;
hence  ( {} <> dom fi implies sup (C +^ fi) = C +^ (sup fi) ) by A1, Th39; ::_thesis: verum
end;

theorem Th44: :: ORDINAL3:44
for fi being Ordinal-Sequence
for C being Ordinal st {} <> dom fi & C <> {} & sup fi is limit_ordinal holds
sup (fi *^ C) = (sup fi) *^ C
proof
let fi be Ordinal-Sequence; ::_thesis: for C being Ordinal st {} <> dom fi & C <> {} & sup fi is limit_ordinal holds
sup (fi *^ C) = (sup fi) *^ C
let C be Ordinal; ::_thesis: ( {} <> dom fi & C <> {} & sup fi is limit_ordinal implies sup (fi *^ C) = (sup fi) *^ C )
A1: for A, B being Ordinal st A in dom fi & B = fi . A holds
(fi *^ C) . A = B *^ C by Def4;
 dom (fi *^ C) = dom fi by Def4;
hence  ( {} <> dom fi & C <> {} & sup fi is limit_ordinal implies sup (fi *^ C) = (sup fi) *^ C ) by A1, Th42; ::_thesis: verum
end;

theorem Th45: :: ORDINAL3:45
for B, A being Ordinal st B <> {} holds
union (A +^ B) = A +^ (union B)
proof
let B, A be Ordinal; ::_thesis: ( B <> {} implies union (A +^ B) = A +^ (union B) )
assume A1: B <> {} ; ::_thesis: union (A +^ B) = A +^ (union B)
A2: now__::_thesis:_(_(_for_C_being_Ordinal_holds_not_B_=_succ_C_)_implies_union_(A_+^_B)_=_A_+^_(union_B)_)
assume  for C being Ordinal holds not B = succ C ; ::_thesis: union (A +^ B) = A +^ (union B)
then A3: B is limit_ordinal by ORDINAL1:29;
then  A +^ B is limit_ordinal by A1, Th29;
then  union (A +^ B) = A +^ B by ORDINAL1:def_6;
hence  union (A +^ B) = A +^ (union B) by A3, ORDINAL1:def_6; ::_thesis: verum
end;
now__::_thesis:_(_ex_C_being_Ordinal_st_B_=_succ_C_implies_union_(A_+^_B)_=_A_+^_(union_B)_)
given C being Ordinal such that A4: B = succ C ; ::_thesis: union (A +^ B) = A +^ (union B)
thus  union (A +^ B) = union (succ (A +^ C)) by A4, ORDINAL2:28
.= A +^ C by ORDINAL2:2
.= A +^ (union B) by A4, ORDINAL2:2 ; ::_thesis: verum
end;
hence  union (A +^ B) = A +^ (union B) by A2; ::_thesis: verum
end;

theorem Th46: :: ORDINAL3:46
for A, B, C being Ordinal holds (A +^ B) *^ C = (A *^ C) +^ (B *^ C)
proof
let A, B, C be Ordinal; ::_thesis: (A +^ B) *^ C = (A *^ C) +^ (B *^ C)
defpred S1[ Ordinal] means (A +^ $1) *^ C = (A *^ C) +^ ($1 *^ C);
A1: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
assume A2: (A +^ B) *^ C = (A *^ C) +^ (B *^ C) ; ::_thesis: S1[ succ B]
thus (A +^ (succ B)) *^ C = (succ (A +^ B)) *^ C by ORDINAL2:28
.= ((A *^ C) +^ (B *^ C)) +^ C by A2, ORDINAL2:36
.= (A *^ C) +^ ((B *^ C) +^ C) by Th30
.= (A *^ C) +^ ((succ B) *^ C) by ORDINAL2:36 ; ::_thesis: verum
end;
A3: for B being Ordinal st B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
deffunc H1( Ordinal) ->  set = A +^ $1;
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that
A4: B <> {} and
A5: B is limit_ordinal and
A6: for D being Ordinal st D in B holds
S1[D] ; ::_thesis: S1[B]
consider fi being Ordinal-Sequence such that
A7: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
 A +^ B is limit_ordinal by A4, A5, Th29;
then A8: (A +^ B) *^ C is limit_ordinal by Th40;
A9: dom (fi *^ C) = dom fi by Def4;
A10: now__::_thesis:_(_C_=_{}_implies_S1[B]_)
assume A11: C = {} ; ::_thesis: S1[B]
then A12: A *^ C = {} by ORDINAL2:38;
A13: B *^ C = {} by A11, ORDINAL2:38;
 (A +^ B) *^ C = {} by A11, ORDINAL2:38;
hence  S1[B] by A12, A13, ORDINAL2:27; ::_thesis: verum
end;
deffunc H2( Ordinal) ->  set = $1 *^ C;
consider psi being Ordinal-Sequence such that
A14: ( dom psi = B & ( for D being Ordinal st D in B holds
psi . D = H2(D) ) ) from ORDINAL2:sch_3();
A15: now__::_thesis:_for_x_being_set_st_x_in_B_holds_
(fi_*^_C)_._x_=_((A_*^_C)_+^_psi)_._x
let x be set ; ::_thesis: ( x in B implies (fi *^ C) . x = ((A *^ C) +^ psi) . x )
assume A16: x in B ; ::_thesis: (fi *^ C) . x = ((A *^ C) +^ psi) . x
then reconsider k = x as Ordinal ;
reconsider m = fi . k, n = psi . k as Ordinal ;
thus (fi *^ C) . x = m *^ C by A7, A16, Def4
.= (A +^ k) *^ C by A7, A16
.= (A *^ C) +^ (k *^ C) by A6, A16
.= (A *^ C) +^ n by A14, A16
.= ((A *^ C) +^ psi) . x by A14, A16, Def1 ; ::_thesis: verum
end;
reconsider k = psi . {} as Ordinal ;
 {} in B by A4, Th8;
then  k in rng psi by A14, FUNCT_1:def_3;
then A17: k in sup (rng psi) by ORDINAL2:19;
 dom ((A *^ C) +^ psi) = dom psi by Def1;
then A18: fi *^ C = (A *^ C) +^ psi by A7, A14, A9, A15, FUNCT_1:2;
A19: A +^ B = sup fi by A4, A5, A7, ORDINAL2:29;
now__::_thesis:_(_C_<>_{}_implies_(A_+^_B)_*^_C_=_(A_*^_C)_+^_(B_*^_C)_)
assume  C <> {} ; ::_thesis: (A +^ B) *^ C = (A *^ C) +^ (B *^ C)
then (A +^ B) *^ C = sup (fi *^ C) by A4, A5, A7, A19, Th29, Th44
.= (A *^ C) +^ (sup psi) by A4, A14, A18, Th43 ;
hence (A +^ B) *^ C = union ((A *^ C) +^ (sup psi)) by A8, ORDINAL1:def_6
.= (A *^ C) +^ (union (sup psi)) by A17, Th45
.= (A *^ C) +^ (B *^ C) by A4, A5, A14, ORDINAL2:37 ;
::_thesis: verum
end;
hence  S1[B] by A10; ::_thesis: verum
end;
(A +^ {}) *^ C = A *^ C by ORDINAL2:27
.= (A *^ C) +^ {} by ORDINAL2:27
.= (A *^ C) +^ ({} *^ C) by ORDINAL2:35 ;
then A20: S1[ {} ] ;
 for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A20, A1, A3);
hence  (A +^ B) *^ C = (A *^ C) +^ (B *^ C) ; ::_thesis: verum
end;

theorem Th47: :: ORDINAL3:47
for A, B being Ordinal st A <> {} holds
ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )
proof
let A, B be Ordinal; ::_thesis: ( A <> {} implies ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A ) )
defpred S1[ Ordinal] means  ex C, D being Ordinal st
( $1 = (C *^ A) +^ D & D in A );
assume A1: A <> {} ; ::_thesis: ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )
A2: for B being Ordinal st B <> {} & B is limit_ordinal & ( for A being Ordinal st A in B holds
S1[A] ) holds
S1[B]
proof
 {} in A by A1, Th8;
then A3: succ {} c= A by ORDINAL1:21;
let B be Ordinal; ::_thesis: ( B <> {} & B is limit_ordinal & ( for A being Ordinal st A in B holds
S1[A] ) implies S1[B] )
assume that
 B <> {} and
A4: B is limit_ordinal and
 for A being Ordinal st A in B holds
S1[A] ; ::_thesis: S1[B]
defpred S2[ Ordinal] means ( $1 in B & B in $1 *^ A );
 B *^ 1 = B by ORDINAL2:39;
then A5: B c= B *^ A by A3, ORDINAL2:42;
A6: now__::_thesis:_(_B_<>_B_*^_A_implies_S1[B]_)
assume  B <> B *^ A ; ::_thesis: S1[B]
then  B c< B *^ A by A5, XBOOLE_0:def_8;
then  B in B *^ A by ORDINAL1:11;
then A7: ex C being Ordinal st S2[C] by A4, Th41;
consider C being Ordinal such that
A8: S2[C] and
A9: for C1 being Ordinal st S2[C1] holds
C c= C1 from ORDINAL1:sch_1(A7);
now__::_thesis:_not_C_is_limit_ordinal
assume  C is limit_ordinal ; ::_thesis: contradiction
then consider C1 being Ordinal such that
A10: C1 in C and
A11: B in C1 *^ A by A8, Th41;
 C1 in B by A8, A10, ORDINAL1:10;
hence  contradiction by A9, A10, A11, ORDINAL1:5; ::_thesis: verum
end;
then consider C1 being Ordinal such that
A12: C = succ C1 by ORDINAL1:29;
A13: C1 in C by A12, ORDINAL1:6;
then  C1 in B by A8, ORDINAL1:10;
then  not B in C1 *^ A by A9, A13, ORDINAL1:5;
then consider D being Ordinal such that
A14: B = (C1 *^ A) +^ D by Th27, ORDINAL1:16;
thus  S1[B] ::_thesis: verum
proof
take  C1 ; ::_thesis: ex D being Ordinal st
( B = (C1 *^ A) +^ D & D in A )
take  D ; ::_thesis: ( B = (C1 *^ A) +^ D & D in A )
thus  B = (C1 *^ A) +^ D by A14; ::_thesis: D in A
 (C1 *^ A) +^ D in (C1 *^ A) +^ A by A8, A12, A14, ORDINAL2:36;
hence  D in A by Th22; ::_thesis: verum
end;
end;
 ( B = B *^ A implies ( B = (B *^ A) +^ {} & {} in A ) ) by A1, Th8, ORDINAL2:27;
hence  S1[B] by A6; ::_thesis: verum
end;
A15: for B being Ordinal st S1[B] holds
S1[ succ B]
proof
let B be Ordinal; ::_thesis: ( S1[B] implies S1[ succ B] )
given C, D being Ordinal such that A16: B = (C *^ A) +^ D and
A17: D in A ; ::_thesis: S1[ succ B]
A18: now__::_thesis:_(_not_succ_D_in_A_implies_ex_C1_being_set_ex_D1_being_set_st_
(_(C1_*^_A)_+^_D1_=_succ_B_&_D1_in_A_)_)
assume  not succ D in A ; ::_thesis: ex C1 being set ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A )
then A19: A c= succ D by ORDINAL1:16;
take C1 = succ C; ::_thesis: ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A )
take D1 = {} ; ::_thesis: ( (C1 *^ A) +^ D1 = succ B & D1 in A )
 succ D c= A by A17, ORDINAL1:21;
then A20: A = succ D by A19, XBOOLE_0:def_10;
thus (C1 *^ A) +^ D1 = C1 *^ A by ORDINAL2:27
.= (C *^ A) +^ A by ORDINAL2:36
.= succ B by A16, A20, ORDINAL2:28 ; ::_thesis: D1 in A
thus  D1 in A by A1, Th8; ::_thesis: verum
end;
now__::_thesis:_(_succ_D_in_A_implies_ex_C1_being_Ordinal_ex_D1_being_set_st_
(_(C1_*^_A)_+^_D1_=_succ_B_&_D1_in_A_)_)
assume A21: succ D in A ; ::_thesis: ex C1 being Ordinal ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A )
take C1 = C; ::_thesis: ex D1 being set st
( (C1 *^ A) +^ D1 = succ B & D1 in A )
take D1 = succ D; ::_thesis: ( (C1 *^ A) +^ D1 = succ B & D1 in A )
thus  (C1 *^ A) +^ D1 = succ B by A16, ORDINAL2:28; ::_thesis: D1 in A
thus  D1 in A by A21; ::_thesis: verum
end;
hence  S1[ succ B] by A18; ::_thesis: verum
end;
A22: S1[ {} ]
proof
take C = {} ; ::_thesis: ex D being Ordinal st
( {} = (C *^ A) +^ D & D in A )
take D = {} ; ::_thesis: ( {} = (C *^ A) +^ D & D in A )
thus  {} = {} +^ {} by ORDINAL2:27
.= (C *^ A) +^ D by ORDINAL2:35 ; ::_thesis: D in A
thus  D in A by A1, Th8; ::_thesis: verum
end;
 for B being Ordinal holds S1[B] from ORDINAL2:sch_1(A22, A15, A2);
hence  ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A ) ; ::_thesis: verum
end;

theorem Th48: :: ORDINAL3:48
for A, C1, D1, C2, D2 being Ordinal st (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 & D1 in A & D2 in A holds
( C1 = C2 & D1 = D2 )
proof
let A be Ordinal; ::_thesis: for C1, D1, C2, D2 being Ordinal st (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 & D1 in A & D2 in A holds
( C1 = C2 & D1 = D2 )
let C1, D1, C2, D2 be Ordinal; ::_thesis: ( (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 & D1 in A & D2 in A implies ( C1 = C2 & D1 = D2 ) )
assume that
A1: (C1 *^ A) +^ D1 = (C2 *^ A) +^ D2 and
A2: D1 in A and
A3: D2 in A ; ::_thesis: ( C1 = C2 & D1 = D2 )
set B = (C1 *^ A) +^ D1;
A4: now__::_thesis:_not_C2_in_C1
assume  C2 in C1 ; ::_thesis: contradiction
then consider C being Ordinal such that
A5: C1 = C2 +^ C and
A6: C <> {} by Th28;
(C1 *^ A) +^ D1 = ((C2 *^ A) +^ (C *^ A)) +^ D1 by A5, Th46
.= (C2 *^ A) +^ ((C *^ A) +^ D1) by Th30 ;
then A7: D2 = (C *^ A) +^ D1 by A1, Th21;
A8: C *^ A c= (C *^ A) +^ D1 by Th24;
 A c= C *^ A by A6, Th36;
hence  contradiction by A3, A7, A8, ORDINAL1:5; ::_thesis: verum
end;
now__::_thesis:_not_C1_in_C2
assume  C1 in C2 ; ::_thesis: contradiction
then consider C being Ordinal such that
A9: C2 = C1 +^ C and
A10: C <> {} by Th28;
(C1 *^ A) +^ D1 = ((C1 *^ A) +^ (C *^ A)) +^ D2 by A1, A9, Th46
.= (C1 *^ A) +^ ((C *^ A) +^ D2) by Th30 ;
then A11: D1 = (C *^ A) +^ D2 by Th21;
A12: C *^ A c= (C *^ A) +^ D2 by Th24;
 A c= C *^ A by A10, Th36;
hence  contradiction by A2, A11, A12, ORDINAL1:5; ::_thesis: verum
end;
hence  C1 = C2 by A4, ORDINAL1:14; ::_thesis: D1 = D2
hence  D1 = D2 by A1, Th21; ::_thesis: verum
end;

theorem Th49: :: ORDINAL3:49
for B, A being Ordinal st 1 in B & A <> {} & A is limit_ordinal holds
for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) holds
A *^ B = sup fi
proof
let B, A be Ordinal; ::_thesis: ( 1 in B & A <> {} & A is limit_ordinal implies for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) holds
A *^ B = sup fi )
assume that
A1: 1 in B and
A2: A <> {} and
A3: A is limit_ordinal ; ::_thesis: for fi being Ordinal-Sequence st dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) holds
A *^ B = sup fi
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = A & ( for C being Ordinal st C in A holds
fi . C = C *^ B ) implies A *^ B = sup fi )
assume that
A4: dom fi = A and
A5: for C being Ordinal st C in A holds
fi . C = C *^ B ; ::_thesis: A *^ B = sup fi
now__::_thesis:_for_C_being_Ordinal_holds_not_sup_fi_=_succ_C
given C being Ordinal such that A6: sup fi = succ C ; ::_thesis: contradiction
consider D being Ordinal such that
A7: D in rng fi and
A8: C c= D by A6, ORDINAL1:6, ORDINAL2:21;
 D in sup fi by A7, ORDINAL2:19;
then A9: succ D c= succ C by A6, ORDINAL1:21;
 succ C c= succ D by A8, ORDINAL2:1;
then  succ C = succ D by A9, XBOOLE_0:def_10;
then  C = D by ORDINAL1:7;
then consider x being set  such that
A10: x in dom fi and
A11: C = fi . x by A7, FUNCT_1:def_3;
reconsider x = x as Ordinal by A10;
A12: C = x *^ B by A4, A5, A10, A11;
 C +^ 1 in C +^ B by A1, ORDINAL2:32;
then A13: sup fi in C +^ B by A6, ORDINAL2:31;
A14: (succ x) *^ B = (x *^ B) +^ B by ORDINAL2:36;
A15: succ x in dom fi by A3, A4, A10, ORDINAL1:28;
then  fi . (succ x) = (succ x) *^ B by A4, A5;
then  C +^ B in rng fi by A15, A12, A14, FUNCT_1:def_3;
hence  contradiction by A13, ORDINAL2:19; ::_thesis: verum
end;
then A16: sup fi is limit_ordinal by ORDINAL1:29;
 A *^ B = union (sup fi) by A2, A3, A4, A5, ORDINAL2:37;
hence  A *^ B = sup fi by A16, ORDINAL1:def_6; ::_thesis: verum
end;

theorem :: ORDINAL3:50
for A, B, C being Ordinal holds (A *^ B) *^ C = A *^ (B *^ C)
proof
let A, B, C be Ordinal; ::_thesis: (A *^ B) *^ C = A *^ (B *^ C)
defpred S1[ Ordinal] means ($1 *^ B) *^ C = $1 *^ (B *^ C);
A1: {} *^ C = {} by ORDINAL2:35;
A2: for A being Ordinal st S1[A] holds
S1[ succ A]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume A3: (A *^ B) *^ C = A *^ (B *^ C) ; ::_thesis: S1[ succ A]
thus ((succ A) *^ B) *^ C = ((A *^ B) +^ B) *^ C by ORDINAL2:36
.= (A *^ (B *^ C)) +^ (B *^ C) by A3, Th46
.= (A *^ (B *^ C)) +^ (1 *^ (B *^ C)) by ORDINAL2:39
.= (A +^ 1) *^ (B *^ C) by Th46
.= (succ A) *^ (B *^ C) by ORDINAL2:31 ; ::_thesis: verum
end;
A4: for A being Ordinal st A <> {} & A is limit_ordinal & ( for D being Ordinal st D in A holds
S1[D] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for D being Ordinal st D in A holds
S1[D] ) implies S1[A] )
assume that
A5: A <> {} and
A6: A is limit_ordinal and
A7: for D being Ordinal st D in A holds
(D *^ B) *^ C = D *^ (B *^ C) ; ::_thesis: S1[A]
A8: now__::_thesis:_(_1_in_B_&_1_in_C_implies_S1[A]_)
deffunc H1( Ordinal) ->  set = $1 *^ B;
assume that
A9: 1 in B and
A10: 1 in C ; ::_thesis: S1[A]
consider fi being Ordinal-Sequence such that
A11: ( dom fi = A & ( for D being Ordinal st D in A holds
fi . D = H1(D) ) ) from ORDINAL2:sch_3();
A12: ( dom (fi *^ C) = A & ( for D being Ordinal st D in A holds
(fi *^ C) . D = D *^ (B *^ C) ) )
proof
thus  dom (fi *^ C) = A by A11, Def4; ::_thesis: for D being Ordinal st D in A holds
(fi *^ C) . D = D *^ (B *^ C)
let D be Ordinal; ::_thesis: ( D in A implies (fi *^ C) . D = D *^ (B *^ C) )
assume A13: D in A ; ::_thesis: (fi *^ C) . D = D *^ (B *^ C)
then A14: fi . D = D *^ B by A11;
 (fi *^ C) . D = (fi . D) *^ C by A11, A13, Def4;
hence  (fi *^ C) . D = D *^ (B *^ C) by A7, A13, A14; ::_thesis: verum
end;
 1 = 1 *^ 1 by ORDINAL2:39;
then  1 in B *^ C by A9, A10, Th19;
then A15: A *^ (B *^ C) = sup (fi *^ C) by A5, A6, A12, Th49;
 A *^ B = sup fi by A5, A6, A9, A11, Th49;
hence  S1[A] by A5, A6, A10, A11, A15, Th40, Th44; ::_thesis: verum
end;
now__::_thesis:_(_(_not_1_in_B_or_not_1_in_C_)_implies_S1[A]_)
assume  ( not 1 in B or not 1 in C ) ; ::_thesis: S1[A]
then A16: ( B = {} or B = 1 or C = {} or C = 1 ) by Th16, ORDINAL1:16;
A17: {} *^ C = {} by ORDINAL2:35;
A18: (A *^ B) *^ 1 = A *^ B by ORDINAL2:39;
A19: (A *^ B) *^ {} = {} by ORDINAL2:38;
A20: A *^ 1 = A by ORDINAL2:39;
 A *^ {} = {} by ORDINAL2:38;
hence  S1[A] by A16, A17, A20, A19, A18, ORDINAL2:38, ORDINAL2:39; ::_thesis: verum
end;
hence  S1[A] by A8; ::_thesis: verum
end;
 {} *^ B = {} by ORDINAL2:35;
then A21: S1[ {} ] by A1, ORDINAL2:35;
 for A being Ordinal holds S1[A] from ORDINAL2:sch_1(A21, A2, A4);
hence  (A *^ B) *^ C = A *^ (B *^ C) ; ::_thesis: verum
end;

definition
let A, B be Ordinal;
funcA -^ B ->  Ordinal means :Def5: :: ORDINAL3:def 5
A = B +^ it if B c= A
otherwise it = {} ;
existence
 ( ( B c= A implies ex b1 being Ordinal st A = B +^ b1 ) & ( not B c= A implies ex b1 being Ordinal st b1 = {} ) ) by Th27;
uniqueness
 for b1, b2 being Ordinal holds
( ( B c= A & A = B +^ b1 & A = B +^ b2 implies b1 = b2 ) & ( not B c= A & b1 = {} & b2 = {} implies b1 = b2 ) ) by Th21;
consistency
 for b1 being Ordinal holds verum ;
funcA div^ B ->  Ordinal means :Def6: :: ORDINAL3:def 6
 ex C being Ordinal st
( A = (it *^ B) +^ C & C in B ) if B <> {}
otherwise it = {} ;
consistency
 for b1 being Ordinal holds verum ;
existence
 ( ( B <> {} implies ex b1, C being Ordinal st
( A = (b1 *^ B) +^ C & C in B ) ) & ( not B <> {} implies ex b1 being Ordinal st b1 = {} ) ) by Th47;
uniqueness
 for b1, b2 being Ordinal holds
( ( B <> {} & ex C being Ordinal st
( A = (b1 *^ B) +^ C & C in B ) & ex C being Ordinal st
( A = (b2 *^ B) +^ C & C in B ) implies b1 = b2 ) & ( not B <> {} & b1 = {} & b2 = {} implies b1 = b2 ) ) by Th48;
end;

:: deftheorem Def5 defines -^ ORDINAL3:def_5_:_
 for A, B, b3 being Ordinal holds
( ( B c= A implies ( b3 = A -^ B iff A = B +^ b3 ) ) & ( not B c= A implies ( b3 = A -^ B iff b3 = {} ) ) );

:: deftheorem Def6 defines div^ ORDINAL3:def_6_:_
 for A, B, b3 being Ordinal holds
( ( B <> {} implies ( b3 = A div^ B iff ex C being Ordinal st
( A = (b3 *^ B) +^ C & C in B ) ) ) & ( not B <> {} implies ( b3 = A div^ B iff b3 = {} ) ) );

definition
let A, B be Ordinal;
funcA mod^ B ->  Ordinal equals :: ORDINAL3:def 7
A -^ ((A div^ B) *^ B);
correctness
coherence
A -^ ((A div^ B) *^ B) is Ordinal;
;
end;

:: deftheorem  defines mod^ ORDINAL3:def_7_:_
 for A, B being Ordinal holds A mod^ B = A -^ ((A div^ B) *^ B);

theorem :: ORDINAL3:51
for A, B being Ordinal st A in B holds
B = A +^ (B -^ A)
proof
let A, B be Ordinal; ::_thesis: ( A in B implies B = A +^ (B -^ A) )
assume  A in B ; ::_thesis: B = A +^ (B -^ A)
then  A c= B by ORDINAL1:def_2;
hence  B = A +^ (B -^ A) by Def5; ::_thesis: verum
end;

theorem Th52: :: ORDINAL3:52
for A, B being Ordinal holds (A +^ B) -^ A = B
proof
let A, B be Ordinal; ::_thesis: (A +^ B) -^ A = B
 A c= A +^ B by Th24;
hence  (A +^ B) -^ A = B by Def5; ::_thesis: verum
end;

theorem Th53: :: ORDINAL3:53
for A, B, C being Ordinal st A in B & ( C c= A or C in A ) holds
A -^ C in B -^ C
proof
let A, B, C be Ordinal; ::_thesis: ( A in B & ( C c= A or C in A ) implies A -^ C in B -^ C )
assume that
A1: A in B and
A2: ( C c= A or C in A ) ; ::_thesis: A -^ C in B -^ C
 A c= B by A1, ORDINAL1:def_2;
then  C c= B by A2, ORDINAL1:def_2, XBOOLE_1:1;
then A3: B = C +^ (B -^ C) by Def5;
 C c= A by A2, ORDINAL1:def_2;
then  A = C +^ (A -^ C) by Def5;
hence  A -^ C in B -^ C by A1, A3, Th22; ::_thesis: verum
end;

theorem Th54: :: ORDINAL3:54
for A being Ordinal holds A -^ A = {}
proof
let A be Ordinal; ::_thesis: A -^ A = {}
 A +^ {} = A by ORDINAL2:27;
hence  A -^ A = {} by Def5; ::_thesis: verum
end;

theorem :: ORDINAL3:55
for A, B being Ordinal st A in B holds
( B -^ A <> {} & {} in B -^ A )
proof
let A, B be Ordinal; ::_thesis: ( A in B implies ( B -^ A <> {} & {} in B -^ A ) )
assume  A in B ; ::_thesis: ( B -^ A <> {} & {} in B -^ A )
then  A -^ A in B -^ A by Th53;
hence  ( B -^ A <> {} & {} in B -^ A ) by Th54; ::_thesis: verum
end;

theorem Th56: :: ORDINAL3:56
for A being Ordinal holds
( A -^ {} = A & {} -^ A = {} )
proof
let A be Ordinal; ::_thesis: ( A -^ {} = A & {} -^ A = {} )
A1: {} +^ A = A by ORDINAL2:30;
 {} c= A by XBOOLE_1:2;
hence  A -^ {} = A by A1, Def5; ::_thesis: {} -^ A = {}
 ( not A c= {} or A c= {} ) ;
then  ( {} -^ A = {} or A = {} ) by Def5, XBOOLE_1:3;
hence  {} -^ A = {} by A1, Def5; ::_thesis: verum
end;

theorem :: ORDINAL3:57
for A, B, C being Ordinal holds A -^ (B +^ C) = (A -^ B) -^ C
proof
let A, B, C be Ordinal; ::_thesis: A -^ (B +^ C) = (A -^ B) -^ C
now__::_thesis:_A_-^_(B_+^_C)_=_(A_-^_B)_-^_C
percases ( B +^ C c= A or not B +^ C c= A ) ;
suppose B +^ C c= A ; ::_thesis: A -^ (B +^ C) = (A -^ B) -^ C
then  A = (B +^ C) +^ (A -^ (B +^ C)) by Def5;
then  A = B +^ (C +^ (A -^ (B +^ C))) by Th30;
then  C +^ (A -^ (B +^ C)) = A -^ B by Th52;
hence  A -^ (B +^ C) = (A -^ B) -^ C by Th52; ::_thesis: verum
end;
supposeA1: not B +^ C c= A ; ::_thesis: A -^ (B +^ C) = (A -^ B) -^ C
A2: now__::_thesis:_(_A_=_B_+^_(A_-^_B)_implies_(A_-^_B)_-^_C_=_{}_)
assume  A = B +^ (A -^ B) ; ::_thesis: (A -^ B) -^ C = {}
then  not C c= A -^ B by A1, ORDINAL2:33;
hence  (A -^ B) -^ C = {} by Def5; ::_thesis: verum
end;
 ( B c= A or not B c= A ) ;
then A3: ( A = B +^ (A -^ B) or A -^ B = {} ) by Def5;
 A -^ (B +^ C) = {} by A1, Def5;
hence  A -^ (B +^ C) = (A -^ B) -^ C by A3, A2, Th56; ::_thesis: verum
end;
end;
end;
hence  A -^ (B +^ C) = (A -^ B) -^ C ; ::_thesis: verum
end;

theorem :: ORDINAL3:58
for A, B, C being Ordinal st A c= B holds
C -^ B c= C -^ A
proof
let A, B, C be Ordinal; ::_thesis: ( A c= B implies C -^ B c= C -^ A )
assume A1: A c= B ; ::_thesis: C -^ B c= C -^ A
then A2: B = A +^ (B -^ A) by Def5;
A3: now__::_thesis:_(_B_c=_C_implies_C_-^_B_c=_C_-^_A_)
assume A4: B c= C ; ::_thesis: C -^ B c= C -^ A
then A5: C = B +^ (C -^ B) by Def5;
 A c= C by A1, A4, XBOOLE_1:1;
then  B +^ (C -^ B) = A +^ (C -^ A) by A5, Def5;
then  A +^ ((B -^ A) +^ (C -^ B)) = A +^ (C -^ A) by A2, Th30;
then  (B -^ A) +^ (C -^ B) = C -^ A by Th21;
hence  C -^ B c= C -^ A by Th24; ::_thesis: verum
end;
now__::_thesis:_(_not_B_c=_C_implies_C_-^_B_c=_C_-^_A_)
assume  not B c= C ; ::_thesis: C -^ B c= C -^ A
then  C -^ B = {} by Def5;
hence  C -^ B c= C -^ A by XBOOLE_1:2; ::_thesis: verum
end;
hence  C -^ B c= C -^ A by A3; ::_thesis: verum
end;

theorem :: ORDINAL3:59
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_c=_A_implies_A_-^_C_c=_B_-^_C_)
assume A3: C c= A ; ::_thesis: A -^ C c= B -^ C
then A4: A = C +^ (A -^ C) by Def5;
 C c= B by A1, A3, XBOOLE_1:1;
then  C +^ (A -^ C) c= C +^ (B -^ C) by A1, A4, Def5;
hence  A -^ C c= B -^ C by Th23; ::_thesis: verum
end;
now__::_thesis:_(_not_C_c=_A_implies_A_-^_C_c=_B_-^_C_)
assume  not C c= A ; ::_thesis: A -^ C c= B -^ C
then  A -^ C = {} by Def5;
hence  A -^ C c= B -^ C by XBOOLE_1:2; ::_thesis: verum
end;
hence  A -^ C c= B -^ C by A2; ::_thesis: verum
end;

theorem :: ORDINAL3:60
for C, A, B being Ordinal st C <> {} & A in B +^ C holds
A -^ B in C
proof
let C, A, B be Ordinal; ::_thesis: ( C <> {} & A in B +^ C implies A -^ B in C )
assume A1: C <> {} ; ::_thesis: ( not A in B +^ C or A -^ B in C )
A2: (B +^ C) -^ B = C by Th52;
 ( not B c= A implies A -^ B = {} ) by Def5;
hence  ( not A in B +^ C or A -^ B in C ) by A1, A2, Th8, Th53; ::_thesis: verum
end;

theorem :: ORDINAL3:61
for A, B, C being Ordinal st A +^ B in C holds
B in C -^ A
proof
let A, B, C be Ordinal; ::_thesis: ( A +^ B in C implies B in C -^ A )
A1: (A +^ B) -^ A = B by Th52;
 A c= A +^ B by Th24;
hence  ( A +^ B in C implies B in C -^ A ) by A1, Th53; ::_thesis: verum
end;

theorem :: ORDINAL3:62
for A, B being Ordinal holds A c= B +^ (A -^ B)
proof
let A, B be Ordinal; ::_thesis: A c= B +^ (A -^ B)
now__::_thesis:_A_c=_B_+^_(A_-^_B)
percases ( B c= A or not B c= A ) ;
suppose B c= A ; ::_thesis: A c= B +^ (A -^ B)
hence  A c= B +^ (A -^ B) by Def5; ::_thesis: verum
end;
supposeA1: not B c= A ; ::_thesis: A c= B +^ (A -^ B)
then  A -^ B = {} by Def5;
hence  A c= B +^ (A -^ B) by A1, ORDINAL2:27; ::_thesis: verum
end;
end;
end;
hence  A c= B +^ (A -^ B) ; ::_thesis: verum
end;

theorem :: ORDINAL3:63
for A, C, B being Ordinal holds (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
proof
let A, C, B be Ordinal; ::_thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
A1: now__::_thesis:_(_not_B_c=_A_implies_(A_*^_C)_-^_(B_*^_C)_=_(A_-^_B)_*^_C_)
assume A2: not B c= A ; ::_thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
then A3: ( not B *^ C c= A *^ C or C = {} ) by Th35;
A4: {} *^ C = {} by ORDINAL2:35;
A5: A *^ {} = {} by ORDINAL2:38;
 A -^ B = {} by A2, Def5;
hence  (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by A3, A5, A4, Def5, Th56; ::_thesis: verum
end;
now__::_thesis:_(_B_c=_A_implies_(A_*^_C)_-^_(B_*^_C)_=_(A_-^_B)_*^_C_)
assume  B c= A ; ::_thesis: (A *^ C) -^ (B *^ C) = (A -^ B) *^ C
then  A = B +^ (A -^ B) by Def5;
then  A *^ C = (B *^ C) +^ ((A -^ B) *^ C) by Th46;
hence  (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by Th52; ::_thesis: verum
end;
hence  (A *^ C) -^ (B *^ C) = (A -^ B) *^ C by A1; ::_thesis: verum
end;

theorem Th64: :: ORDINAL3:64
for A, B being Ordinal holds (A div^ B) *^ B c= A
proof
let A, B be Ordinal; ::_thesis: (A div^ B) *^ B c= A
now__::_thesis:_(A_div^_B)_*^_B_c=_A
percases ( B <> {} or B = {} ) ;
suppose B <> {} ; ::_thesis: (A div^ B) *^ B c= A
then  ex C being Ordinal st
( A = ((A div^ B) *^ B) +^ C & C in B ) by Def6;
hence  (A div^ B) *^ B c= A by Th24; ::_thesis: verum
end;
suppose B = {} ; ::_thesis: (A div^ B) *^ B c= A
then  A div^ B = {} by Def6;
then  (A div^ B) *^ B = {} by ORDINAL2:35;
hence  (A div^ B) *^ B c= A by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
hence  (A div^ B) *^ B c= A ; ::_thesis: verum
end;

theorem Th65: :: ORDINAL3:65
for A, B being Ordinal holds A = ((A div^ B) *^ B) +^ (A mod^ B)
proof
let A, B be Ordinal; ::_thesis: A = ((A div^ B) *^ B) +^ (A mod^ B)
 (A div^ B) *^ B c= A by Th64;
hence  A = ((A div^ B) *^ B) +^ (A mod^ B) by Def5; ::_thesis: verum
end;

theorem :: ORDINAL3:66
for A, B, C, D being Ordinal st A = (B *^ C) +^ D & D in C holds
( B = A div^ C & D = A mod^ C )
proof
let A, B, C, D be Ordinal; ::_thesis: ( A = (B *^ C) +^ D & D in C implies ( B = A div^ C & D = A mod^ C ) )
assume that
A1: A = (B *^ C) +^ D and
A2: D in C ; ::_thesis: ( B = A div^ C & D = A mod^ C )
thus  B = A div^ C by A1, A2, Def6; ::_thesis: D = A mod^ C
hence  D = A mod^ C by A1, Th52; ::_thesis: verum
end;

theorem :: ORDINAL3:67
for A, B, C being Ordinal st A in B *^ C holds
( A div^ C in B & A mod^ C in C )
proof
let A, B, C be Ordinal; ::_thesis: ( A in B *^ C implies ( A div^ C in B & A mod^ C in C ) )
A1: A = ((A div^ C) *^ C) +^ (A mod^ C) by Th65;
assume A2: A in B *^ C ; ::_thesis: ( A div^ C in B & A mod^ C in C )
then  C <> {} by ORDINAL2:38;
then A3: ex D being Ordinal st
( A = ((A div^ C) *^ C) +^ D & D in C ) by Def6;
then A4: (A div^ C) *^ C c= A by Th24;
assume  ( not A div^ C in B or not A mod^ C in C ) ; ::_thesis: contradiction
then  B *^ C c= (A div^ C) *^ C by A3, A1, Th21, ORDINAL1:16, ORDINAL2:41;
hence  contradiction by A2, A4, ORDINAL1:5; ::_thesis: verum
end;

theorem Th68: :: ORDINAL3:68
for B, A being Ordinal st B <> {} holds
(A *^ B) div^ B = A
proof
let B, A be Ordinal; ::_thesis: ( B <> {} implies (A *^ B) div^ B = A )
assume  B <> {} ; ::_thesis: (A *^ B) div^ B = A
then A1: {} in B by Th8;
 A *^ B = (A *^ B) +^ {} by ORDINAL2:27;
hence  (A *^ B) div^ B = A by A1, Def6; ::_thesis: verum
end;

theorem :: ORDINAL3:69
for A, B being Ordinal holds (A *^ B) mod^ B = {}
proof
let A, B be Ordinal; ::_thesis: (A *^ B) mod^ B = {}
A1: A *^ {} = {} by ORDINAL2:38;
A2: (A *^ B) -^ (A *^ B) = {} by Th54;
 {} -^ (((A *^ B) div^ B) *^ B) = {} by Th56;
hence  (A *^ B) mod^ B = {} by A1, A2, Th68; ::_thesis: verum
end;

theorem :: ORDINAL3:70
for A being Ordinal holds
( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )
proof
let A be Ordinal; ::_thesis: ( {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A )
A1: ( A = {} or A <> {} ) ;
 {} = {} *^ A by ORDINAL2:35;
hence  {} div^ A = {} by A1, Def6, Th68; ::_thesis: ( {} mod^ A = {} & A mod^ {} = A )
thus  {} mod^ A = {} by Th56; ::_thesis: A mod^ {} = A
thus A mod^ {} = A -^ {} by ORDINAL2:38
.= A by Th56 ; ::_thesis: verum
end;

theorem :: ORDINAL3:71
for A being Ordinal holds
( A div^ 1 = A & A mod^ 1 = {} )
proof
let A be Ordinal; ::_thesis: ( A div^ 1 = A & A mod^ 1 = {} )
A1: A = A *^ 1 by ORDINAL2:39;
A2: A = A +^ {} by ORDINAL2:27;
A3: {} in 1 by Th8;
hence  A div^ 1 = A by A1, A2, Def6; ::_thesis: A mod^ 1 = {}
thus A mod^ 1 = A -^ A by A1, A2, A3, Def6
.= {} by Th54 ; ::_thesis: verum
end;

begin

theorem :: ORDINAL3:72
for X being set holds sup X c= succ (union (On X))
proof
let X be set ; ::_thesis: sup X c= succ (union (On X))
reconsider A = union (On X) as Ordinal by Th5;
 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 a = x as Ordinal by ORDINAL1:def_9;
 a c= A by A1, ZFMISC_1:74;
hence  x in succ A by ORDINAL1:22; ::_thesis: verum
end;
hence  sup X c= succ (union (On X)) by ORDINAL2:def_3; ::_thesis: verum
end;


theorem :: ORDINAL3:73
for A being Ordinal holds succ A is_cofinal_with 1
proof
let A be Ordinal; ::_thesis: succ A is_cofinal_with 1
deffunc H1( set ) ->  Ordinal = A;
consider psi being Ordinal-Sequence such that
A1: ( dom psi = 1 & ( for B being Ordinal st B in 1 holds
psi . B = H1(B) ) ) from ORDINAL2:sch_3();
take  psi ; :: according to ORDINAL2:def_17 ::_thesis: ( dom psi = 1 & rng psi c= succ A & psi is increasing & succ A = sup psi )
thus  dom psi = 1 by A1; ::_thesis: ( rng psi c= succ A & psi is increasing & succ A = sup psi )
thus  rng psi c= succ A ::_thesis: ( psi is increasing & succ A = sup psi )
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng psi or e in succ A )
assume  e in rng psi ; ::_thesis: e in succ A
then consider u being set  such that
A2: u in 1 and
A3: e = psi . u by A1, FUNCT_1:def_3;
reconsider u = u as Ordinal by A2;
 psi . u = A by A1, A2;
hence  e in succ A by A3, ORDINAL1:6; ::_thesis: verum
end;
thus  psi is increasing ::_thesis: succ A = sup psi
proof
let B be Ordinal; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not B in b1 or not b1 in dom psi or psi . B in psi . b1 )
let C be Ordinal; ::_thesis: ( not B in C or not C in dom psi or psi . B in psi . C )
assume that
A4: B in C and
A5: C in dom psi ; ::_thesis: psi . B in psi . C
thus  psi . B in psi . C by A1, A4, A5, Th14; ::_thesis: verum
end;
A6: psi . {} = A by A1, Lm1, ORDINAL1:6;
 rng psi = {(psi . {})} by A1, Lm1, FUNCT_1:4;
hence  succ A = sup psi by A6, ORDINAL2:23; ::_thesis: verum
end;

theorem Th74: :: ORDINAL3:74
for a, b being Ordinal st a +^ b is natural holds
( a in omega & b in omega )
proof
let x, y be Ordinal; ::_thesis: ( x +^ y is natural implies ( x in omega & y in omega ) )
assume A1: x +^ y in omega ; :: according to ORDINAL1:def_12 ::_thesis: ( x in omega & y in omega )
A2: y c= x +^ y by Th24;
 x c= x +^ y by Th24;
hence  ( x in omega & y in omega ) by A1, A2, ORDINAL1:12; ::_thesis: verum
end;

registration
let a, b be natural Ordinal;
clustera -^ b ->  natural ;
coherence
 a -^ b is natural
proof
 ( not b c= a or b c= a ) ;
then  ( a -^ b = {} or a = b +^ (a -^ b) ) by Def5;
hence  a -^ b in omega by Th74, ORDINAL1:def_11; :: according to ORDINAL1:def_12 ::_thesis: verum
end;
clustera *^ b ->  natural ;
coherence
 a *^ b is natural
proof
defpred S1[ natural Ordinal] means a *^ b is natural ;
A1: now__::_thesis:_for_a_being_natural_Ordinal_st_S1[a]_holds_
S1[_succ_a]
let a be natural Ordinal; ::_thesis: ( S1[a] implies S1[ succ a] )
assume  S1[a] ; ::_thesis: S1[ succ a]
then reconsider c = a *^ b as natural Ordinal ;
 (succ a) *^ b = c +^ b by ORDINAL2:36;
hence  S1[ succ a] ; ::_thesis: verum
end;
A2: S1[ {} ] by ORDINAL2:35;
 S1[a] from ORDINAL2:sch_17(A2, A1);
hence  a *^ b is natural ; ::_thesis: verum
end;
end;

theorem :: ORDINAL3:75
for a, b being Ordinal st a *^ b is natural & not a *^ b is empty holds
( a in omega & b in omega )
proof
let x, y be Ordinal; ::_thesis: ( x *^ y is natural & not x *^ y is empty implies ( x in omega & y in omega ) )
assume A1: x *^ y in omega ; :: according to ORDINAL1:def_12 ::_thesis: ( x *^ y is empty or ( x in omega & y in omega ) )
assume A2: not x *^ y is empty ; ::_thesis: ( x in omega & y in omega )
then  y <> {} by ORDINAL2:38;
then A3: x c= x *^ y by Th36;
 x <> {} by A2, ORDINAL2:35;
then  y c= x *^ y by Th36;
hence  ( x in omega & y in omega ) by A1, A3, ORDINAL1:12; ::_thesis: verum
end;

definition
let a, b be natural Ordinal;
:: original: +^
redefine funca +^ b ->  set ;
commutativity
 for a, b being natural Ordinal holds a +^ b = b +^ a
proof
let a, b be natural Ordinal; ::_thesis: a +^ b = b +^ a
defpred S1[ natural Ordinal] means a +^ $1 = $1 +^ a;
A1: now__::_thesis:_for_b_being_natural_Ordinal_st_S1[b]_holds_
S1[_succ_b]
let b be natural Ordinal; ::_thesis: ( S1[b] implies S1[ succ b] )
assume A2: S1[b] ; ::_thesis: S1[ succ b]
defpred S2[ natural Ordinal] means (succ b) +^ $1 = succ (b +^ $1);
A3: now__::_thesis:_for_a_being_natural_Ordinal_st_S2[a]_holds_
S2[_succ_a]
let a be natural Ordinal; ::_thesis: ( S2[a] implies S2[ succ a] )
assume A4: S2[a] ; ::_thesis: S2[ succ a]
(succ b) +^ (succ a) = succ ((succ b) +^ a) by ORDINAL2:28
.= succ (b +^ (succ a)) by A4, ORDINAL2:28 ;
hence  S2[ succ a] ; ::_thesis: verum
end;
(succ b) +^ {} = succ b by ORDINAL2:27
.= succ (b +^ {}) by ORDINAL2:27 ;
then A5: S2[ {} ] ;
 S2[a] from ORDINAL2:sch_17(A5, A3);
hence  S1[ succ b] by A2, ORDINAL2:28; ::_thesis: verum
end;
a +^ {} = a by ORDINAL2:27
.= {} +^ a by ORDINAL2:30 ;
then A6: S1[ {} ] ;
thus  S1[b] from ORDINAL2:sch_17(A6, A1); ::_thesis: verum
end;
end;

definition
let a, b be natural Ordinal;
:: original: *^
redefine funca *^ b ->  set ;
commutativity
 for a, b being natural Ordinal holds a *^ b = b *^ a
proof
let a, b be natural Ordinal; ::_thesis: a *^ b = b *^ a
defpred S1[ natural Ordinal] means a *^ $1 = $1 *^ a;
A1: now__::_thesis:_for_b_being_natural_Ordinal_st_S1[b]_holds_
S1[_succ_b]
let b be natural Ordinal; ::_thesis: ( S1[b] implies S1[ succ b] )
defpred S2[ natural Ordinal] means $1 *^ (succ b) = ($1 *^ b) +^ $1;
assume A2: S1[b] ; ::_thesis: S1[ succ b]
A3: now__::_thesis:_for_a_being_natural_Ordinal_st_S2[a]_holds_
S2[_succ_a]
let a be natural Ordinal; ::_thesis: ( S2[a] implies S2[ succ a] )
assume A4: S2[a] ; ::_thesis: S2[ succ a]
(succ a) *^ (succ b) = (a *^ (succ b)) +^ (succ b) by ORDINAL2:36
.= (a *^ b) +^ (a +^ (succ b)) by A4, Th30
.= (a *^ b) +^ (succ (a +^ b)) by ORDINAL2:28
.= succ ((a *^ b) +^ (a +^ b)) by ORDINAL2:28
.= succ (((a *^ b) +^ b) +^ a) by Th30
.= succ (((succ a) *^ b) +^ a) by ORDINAL2:36
.= ((succ a) *^ b) +^ (succ a) by ORDINAL2:28 ;
hence  S2[ succ a] ; ::_thesis: verum
end;
{} *^ (succ b) = {} by ORDINAL2:35
.= {} +^ {} by ORDINAL2:27
.= ({} *^ b) +^ {} by ORDINAL2:35 ;
then A5: S2[ {} ] ;
 S2[a] from ORDINAL2:sch_17(A5, A3);
hence  S1[ succ b] by A2, ORDINAL2:36; ::_thesis: verum
end;
a *^ {} = {} by ORDINAL2:38
.= {} *^ a by ORDINAL2:35 ;
then A6: S1[ {} ] ;
thus  S1[b] from ORDINAL2:sch_17(A6, A1); ::_thesis: verum
end;
end;