per cases ( ( a = 0 & b = 0 ) or ( a = 0 & b <> 0 ) or 0 in a ) by ORDINAL3:8;

suppose ( a = 0 & b = 0 ) ; :: thesis: exp (a,b) is Ordinal of U

then exp (a,b) = 1-element_of U by ORDINAL2:43;
hence exp (a,b) is Ordinal of U ; :: thesis: verum

end;

suppose ( a = 0 & b <> 0 ) ; :: thesis: exp (a,b) is Ordinal of U

hence exp (a,b) is Ordinal of U by ORDINAL4:20; :: thesis: verum

end;

suppose AA: 0 in a ; :: thesis: exp (a,b) is Ordinal of U

defpred S₁[ Ordinal] means ( $1 in U implies exp (a,$1) in U );
exp (a,0) = succ 0 by ORDINAL2:43;
then 00: S₁[ {} ] by CLASSES2:5;
01: for b being ordinal number st S₁[b] holds
S₁[ succ b]

proof

let b be ordinal number ; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume that
A1: S₁[b] and
A2: succ b in U ; :: thesis: exp (a,(succ b)) in U
b in succ b by ORDINAL1:6;
then reconsider b = b as Ordinal of U by A2, ORDINAL1:10;
reconsider ab = exp (a,b) as Ordinal of U by A1;
exp (a,(succ b)) = a *^ ab by ORDINAL2:44;
hence exp (a,(succ b)) in U ; :: thesis: verum

end;

02: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be ordinal number ; :: thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) implies S₁[b] )
assume that
B1: ( b <> {} & b is limit_ordinal ) and
B2: for c being ordinal number st c in b holds
S₁[c] and
B0: b in U ; :: thesis: exp (a,b) in U
deffunc H₁( Ordinal) -> set = exp (a,$1);
consider f being Ordinal-Sequence such that
B3: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = H₁(c) ) ) from ORDINAL2:sch 3();
rng f c= On U

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in On U )
assume x in rng f ; :: thesis: x in On U
then consider y being set such that
C1: ( y in b & x = f . y ) by B3, FUNCT_1:def 3;
reconsider y = y as Ordinal by C1;
( S₁[y] & y in U & x = H₁(y) ) by B0, B2, B3, C1, ORDINAL1:10;
hence x in On U by ORDINAL1:def 9; :: thesis: verum

end;

then reconsider f = f as Ordinal-Sequence of b,U by B3, FUNCT_2:2;
B4: exp (a,b) = lim f by B1, B3, ORDINAL2:45;
f is non-decreasing by AA, B3, ORDINAL5:8;
then Union f is_limes_of f by B1, B3, ORDINAL5:6;
then exp (a,b) = Union f by B4, ORDINAL2:def 10;
hence exp (a,b) in U by B0, ThC1; :: thesis: verum

end;

for b being ordinal number holds S₁[b] from ORDINAL2:sch 1(00, 01, 02);
hence exp (a,b) is Ordinal of U ; :: thesis: verum

end;

end;