let a be ordinal number ; :: thesis: ( 0 in a implies exp (a,(a |^|^ omega)) = a |^|^ omega )
assume 0 in a ; :: thesis: exp (a,(a |^|^ omega)) = a |^|^ omega
then ( 1 = succ 0 & succ 0 c= a ) by ORDINAL1:21;
then A1: ( 1 = a or 1 c< a ) by XBOOLE_0:def 8;

per cases ( a = 1 or 1 in a ) by A1, ORDINAL1:11;

suppose A2: a = 1 ; :: thesis: exp (a,(a |^|^ omega)) = a |^|^ omega

hence exp (a,(a |^|^ omega)) = 1 by ORDINAL2:46
.= a |^|^ omega by A2, Th17 ;
:: thesis: verum

end;

suppose A3: 1 in a ; :: thesis: exp (a,(a |^|^ omega)) = a |^|^ omega

deffunc H₁( Ordinal) -> Ordinal = a |^|^ $1;
deffunc H₂( Ordinal) -> set = exp (a,$1);
consider T being Ordinal-Sequence such that
A4: ( dom T = omega & ( for a being ordinal number st a in omega holds
T . a = H₁(a) ) ) from ORDINAL2:sch 3();
consider E being Ordinal-Sequence such that
A5: ( dom E = a |^|^ omega & ( for b being ordinal number st b in a |^|^ omega holds
E . b = H₂(b) ) ) from ORDINAL2:sch 3();
0 in 1 by NAT_1:44;
then ( 0 in a & 0 in omega ) by A3, ORDINAL1:10;
then a c= a |^|^ omega by Th23;
then A6: ( not a |^|^ omega is empty & a |^|^ omega is limit_ordinal ) by A3, Th30;
E is increasing Ordinal-Sequence by A3, A5, ORDINAL4:25;
then ( lim E = exp (a,(a |^|^ omega)) & Union E is_limes_of E ) by A5, A6, Th6, ORDINAL2:45;
then A7: exp (a,(a |^|^ omega)) = Union E by ORDINAL2:def 10;
T is increasing Ordinal-Sequence by A3, A4, Th25;
then ( lim T = a |^|^ omega & Union T is_limes_of T ) by A4, Th15, Th6;
then A8: a |^|^ omega = Union T by ORDINAL2:def 10;
thus exp (a,(a |^|^ omega)) c= a |^|^ omega :: according to XBOOLE_0:def 10 :: thesis: a |^|^ omega c= exp (a,(a |^|^ omega))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in exp (a,(a |^|^ omega)) or x in a |^|^ omega )
assume x in exp (a,(a |^|^ omega)) ; :: thesis: x in a |^|^ omega
then consider b being set such that
A9: ( b in dom E & x in E . b ) by A7, CARD_5:2;
consider c being set such that
A10: ( c in dom T & b in T . c ) by A5, A8, A9, CARD_5:2;
reconsider b = b as Ordinal by A9;
reconsider c = c as Element of omega by A4, A10;
A11: exp (a,b) in exp (a,(T . c)) by A3, A10, ORDINAL4:24;
A12: succ c in omega by ORDINAL1:28;
then ( E . b = H₂(b) & T . c = H₁(c) & T . (succ c) = H₁( succ c) ) by A9, A4, A5;
then E . b in T . (succ c) by A11, Th14;
then x in T . (succ c) by A9, ORDINAL1:10;
hence x in a |^|^ omega by A4, A8, A12, CARD_5:2; :: thesis: verum

end;

thus a |^|^ omega c= exp (a,(a |^|^ omega)) by A3, ORDINAL4:32; :: thesis: verum

end;

end;