let A be Ordinal; :: thesis: ( omega c= A implies 1 +^ A = A )
deffunc H₁( Ordinal) -> set = 1 +^ $1;
consider phi being Ordinal-Sequence such that
A1: ( dom phi = omega & ( for B being Ordinal st B in omega holds
phi . B = H₁(B) ) ) from ORDINAL2:sch 3();
A2: 1 +^ omega = sup phi by A1, Lm2, ORDINAL2:46
.= sup (rng phi) by ORDINAL2:35 ;
A3: 1 +^ omega c= omega

proof

let B be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not B in 1 +^ omega or B in omega )
assume B in 1 +^ omega ; :: thesis: B in omega
then consider C being Ordinal such that
A4: ( C in rng phi & B c= C ) by A2, ORDINAL2:29;
consider x being set such that
A5: ( x in dom phi & C = phi . x ) by A4, FUNCT_1:def 5;
reconsider x = x as Ordinal by A5;
reconsider x' = x as Cardinal by A1, A5;
reconsider x = x as finite Ordinal by A1, A5;
( card (card x) = card x & card (card x) = card x & card x' = x & 0 + 1 = 1 ) by CARD_1:def 5;
then ( x +^ 1 = (card x) + 1 & 1 +^ x = 1 + (card x) ) by CARD_2:49;
then ( C = 1 +^ x & 1 +^ x = x +^ 1 & succ x in omega ) by A1, A5, Lm2, ORDINAL1:41;
then C in omega by ORDINAL2:48;
hence B in omega by A4, ORDINAL1:22; :: thesis: verum

end;

assume omega c= A ; :: thesis: 1 +^ A = A
then A6: ex B being Ordinal st A = omega +^ B by ORDINAL3:30;
omega c= 1 +^ omega by ORDINAL3:27;
then omega = 1 +^ omega by A3, XBOOLE_0:def 10;
hence 1 +^ A = A by A6, ORDINAL3:33; :: thesis: verum