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, Lm5, ORDINAL2:29
.= sup (rng phi) by ORDINAL2:26 ;
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 and
A5: B c= C by A2, ORDINAL2:21;
consider x being set such that
A6: x in dom phi and
A7: C = phi . x by A4, FUNCT_1:def 3;
reconsider x = x as Ordinal by A6;
reconsider x9 = x as Cardinal by A1, A6;
reconsider x = x as finite Ordinal by A1, A6;
A8: card x9 = x by CARD_1:def 2;
then A9: x +^ 1 = (card x) + 1 by Th49;
A10: C = 1 +^ x by A1, A6, A7;
A11: 1 +^ x = x +^ 1 by A8, A9, Th49;
succ x in omega by A1, A6, Lm5, ORDINAL1:28;
then C in omega by A10, A11, ORDINAL2:31;
hence B in omega by A5, ORDINAL1:12; :: thesis: verum

end;

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