let a, b be Ordinal; :: thesis: for x being object st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being Ordinal st
( c in b & x in exp (a,c) ) )
let x be object ; :: thesis: ( 0 in a & not b is empty & b is limit_ordinal implies ( x in exp (a,b) iff ex c being Ordinal st
( c in b & x in exp (a,c) ) ) )
assume A1: ( 0 in a & not b is empty & b is limit_ordinal ) ; :: thesis: ( x in exp (a,b) iff ex c being Ordinal st
( c in b & x in exp (a,c) ) )
deffunc H₁( Ordinal) -> set = exp (a,$1);
consider f being Ordinal-Sequence such that
A2: ( dom f = b & ( for c being Ordinal st c in b holds
f . c = H₁(c) ) ) from ORDINAL2:sch 3();
f is non-decreasing by A1, A2, Th8;
then Union f is_limes_of f by A1, A2, Th6;
then A3: Union f = lim f by ORDINAL2:def 10
.= exp (a,b) by A1, A2, ORDINAL2:45 ;

hereby :: thesis: ( ex c being Ordinal 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 object such that
A4: ( c in dom f & x in f . c ) by A3, CARD_5:2;
reconsider c = c as Ordinal by A4;
take c = c; :: thesis: ( c in b & x in exp (a,c) )
thus c in b by A2, A4; :: thesis: x in exp (a,c)
thus x in exp (a,c) by A2, A4; :: thesis: verum

end;

given c being Ordinal such that A5: ( c in b & x in exp (a,c) ) ; :: thesis: x in exp (a,b)
f . c = H₁(c) by A2, A5;
hence x in exp (a,b) by A2, A3, A5, CARD_5:2; :: thesis: verum