let a, b be ordinal number ; :: thesis: for x being set st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) )
let x be set ; :: thesis: ( 0 in a & not b is empty & b is limit_ordinal implies ( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) ) )
assume Z0: ( 0 in a & not b is empty & b is limit_ordinal ) ; :: thesis: ( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) )
deffunc H₁( Ordinal) -> set = exp (a,$1);
consider f being Ordinal-Sequence such that
Z1: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = H₁(c) ) ) from ORDINAL2:sch 3();
f is non-decreasing by Z0, Z1, Th003;
then Union f is_limes_of f by Z0, Z1, ThND;
then Z2: Union f = lim f by ORDINAL2:def 14
.= exp (a,b) by Z0, Z1, ORDINAL2:62 ;

hereby :: thesis: ( ex c being ordinal number st
( c in b & x in exp (a,c) ) implies x in exp (a,b) )

assume x in exp (a,b) ; :: thesis: ex c being Ordinal st
( c in b & x in exp (a,c) )
then consider c being set such that
Z4: ( c in dom f & x in f . c ) by Z2, CARD_5:10;
reconsider c = c as Ordinal by Z4;
take c = c; :: thesis: ( c in b & x in exp (a,c) )
thus c in b by Z1, Z4; :: thesis: x in exp (a,c)
thus x in exp (a,c) by Z1, Z4; :: thesis: verum

end;

given c being ordinal number such that A1: ( c in b & x in exp (a,c) ) ; :: thesis: x in exp (a,b)
f . c = H₁(c) by Z1, A1;
hence x in exp (a,b) by Z1, Z2, A1, CARD_5:10; :: thesis: verum