let a, b be ordinal number ; :: thesis: ( a is limit_ordinal & 0 in b implies exp a,b is limit_ordinal )
assume A0: ( a is limit_ordinal & 0 in b ) ; :: thesis: exp a,b is limit_ordinal

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

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

hence exp a,b is limit_ordinal by A0, ORDINAL4:20; :: thesis: verum

end;

suppose 0A: 0 in a ; :: thesis: exp a,b is limit_ordinal

defpred S₁[ Ordinal] means ( 0 in $1 implies exp a,$1 is limit_ordinal );
A1: S₁[ {} ] ;
A2: for c being ordinal number st S₁[c] holds
S₁[ succ c]

proof

let c be ordinal number ; :: thesis: ( S₁[c] implies S₁[ succ c] )
exp a,(succ c) = a *^ (exp a,c) by ORDINAL2:61;
hence ( S₁[c] implies S₁[ succ c] ) by A0, ORDINAL3:48; :: thesis: verum

end;

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

proof

let c be ordinal number ; :: thesis: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S₁[b] ) implies S₁[c] )
assume that
Z0: ( c <> {} & c is limit_ordinal ) and
Z1: for b being ordinal number st b in c holds
S₁[b] ; :: thesis: S₁[c]
deffunc H₁( Ordinal) -> set = exp a,$1;
consider f being Ordinal-Sequence such that
B1: ( dom f = c & ( for b being ordinal number st b in c holds
f . b = H₁(b) ) ) from ORDINAL2:sch 3();
B2: exp a,c = lim f by Z0, B1, ORDINAL2:62;
f is non-decreasing by 0A, B1, Th003;
then Union f is_limes_of f by Z0, B1, ThND;
then B3: exp a,c = Union f by B2, ORDINAL2:def 14;
for d being ordinal number st d in exp a,c holds
succ d in exp a,c

proof

let d be ordinal number ; :: 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 set such that
B4: ( b in dom f & d in f . b ) by B3, CARD_5:10;
reconsider b = b as Ordinal by B4;
B5: succ b in dom f by Z0, B1, B4, ORDINAL1:41;
then B6: ( f . b = H₁(b) & f . (succ b) = H₁( succ b) & S₁[ succ b] ) by Z1, B1, B4;
H₁(b) c= H₁( succ b) by 0A, ORDINAL4:27, ORDINAL3:1;
then succ d in f . (succ b) by B6, ORDINAL1:41, B4, ORDINAL3:10;
hence succ d in exp a,c by B3, B5, CARD_5:10; :: thesis: verum

end;

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

end;

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

end;

end;