let a, b be Ordinal; :: thesis: ( a is limit_ordinal & 0 in b implies exp (a,b) is limit_ordinal )
assume A1: ( a is limit_ordinal & 0 in b ) ; :: thesis: exp (a,b) is limit_ordinal

per cases ( a = 0 or 0 in a ) by ORDINAL3:8;

suppose a = 0 ; :: thesis: exp (a,b) is limit_ordinal

hence exp (a,b) is limit_ordinal by A1, ORDINAL4:20; :: thesis: verum

end;

suppose A2: 0 in a ; :: thesis: exp (a,b) is limit_ordinal

defpred S₁[ Ordinal] means ( 0 in $1 implies exp (a,$1) is limit_ordinal );
A3: S₁[ 0 ] ;
A4: for c being Ordinal st S₁[c] holds
S₁[ succ c]

proof

let c be Ordinal; :: thesis: ( S₁[c] implies S₁[ succ c] )
exp (a,(succ c)) = a *^ (exp (a,c)) by ORDINAL2:44;
hence ( S₁[c] implies S₁[ succ c] ) by A1, ORDINAL3:40; :: thesis: verum

end;

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

proof

let c be Ordinal; :: thesis: ( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S₁[b] ) implies S₁[c] )
assume that
A6: ( c <> 0 & c is limit_ordinal ) and
A7: for b being Ordinal st b in c holds
S₁[b] ; :: thesis: S₁[c]
deffunc H₁( Ordinal) -> set = exp (a,$1);
consider f being Ordinal-Sequence such that
A8: ( dom f = c & ( for b being Ordinal st b in c holds
f . b = H₁(b) ) ) from ORDINAL2:sch 3();
A9: exp (a,c) = lim f by A6, A8, ORDINAL2:45;
f is non-decreasing by A2, A8, Th8;
then Union f is_limes_of f by A6, A8, Th6;
then A10: exp (a,c) = Union f by A9, ORDINAL2:def 10;
for d being Ordinal st d in exp (a,c) holds
succ d in exp (a,c)

proof

let d be Ordinal; :: thesis: ( d in exp (a,c) implies succ d in exp (a,c) )
assume d in exp (a,c) ; :: thesis: succ d in exp (a,c)
then consider b being object such that
A11: ( b in dom f & d in f . b ) by A10, CARD_5:2;
reconsider b = b as Ordinal by A11;
A12: succ b in dom f by A6, A8, A11, ORDINAL1:28;
then A13: ( f . b = H₁(b) & f . (succ b) = H₁( succ b) & S₁[ succ b] ) by A7, A8, A11;
H₁(b) c= H₁( succ b) by A2, ORDINAL3:1, ORDINAL4:27;
then succ d in f . (succ b) by A13, A11, ORDINAL1:28, ORDINAL3:8;
hence succ d in exp (a,c) by A10, A12, CARD_5:2; :: thesis: verum

end;

hence S₁[c] by ORDINAL1:28; :: thesis: verum

end;

for c being Ordinal holds S₁[c] from ORDINAL2:sch 1(A3, A4, A5);
hence exp (a,b) is limit_ordinal by A1; :: thesis: verum

end;

end;