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 ; :: thesis: verum

end;

suppose A1: 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 A2: S₁[ 0 ] by CLASSES2:5;
A3: for b being Ordinal st S₁[b] holds
S₁[ succ b]

proof

let b be Ordinal; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume that
A4: S₁[b] and
A5: 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 A5, ORDINAL1:10;
reconsider ab = exp (a,b) as Ordinal of U by A4;
exp (a,(succ b)) = a *^ ab by ORDINAL2:44;
hence exp (a,(succ b)) in U ; :: thesis: verum

end;

A6: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) implies S₁[b] )
assume that
A7: ( b <> 0 & b is limit_ordinal ) and
A8: for c being Ordinal st c in b holds
S₁[c] and
A9: b in U ; :: thesis: exp (a,b) in U
deffunc H₁( Ordinal) -> set = exp (a,$1);
consider f being Ordinal-Sequence such that
A10: ( dom f = b & ( for c being Ordinal st c in b holds
f . c = H₁(c) ) ) from ORDINAL2:sch 3();
rng f c= On U

proof

let x be object ; :: 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 object such that
A11: ( y in b & x = f . y ) by A10, FUNCT_1:def 3;
reconsider y = y as Ordinal by A11;
( S₁[y] & y in U & x = H₁(y) ) by A9, A8, A10, A11, 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 A10, FUNCT_2:2;
A12: exp (a,b) = lim f by A7, A10, ORDINAL2:45;
f is non-decreasing by A1, A10, ORDINAL5:8;
then Union f is_limes_of f by A7, ORDINAL5:6;
then exp (a,b) = Union f by A12, ORDINAL2:def 10;
hence exp (a,b) in U by A9, Th41; :: thesis: verum

end;

for b being Ordinal holds S₁[b] from ORDINAL2:sch 1(A2, A3, A6);
hence exp (a,b) is Ordinal of U ; :: thesis: verum

end;

end;