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, Lm9, 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 object 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: C = 1 +^ x by A1, A6, A7;
succ x in omega by A1, A6, Lm9, ORDINAL1:28;
then C in omega by A8, ORDINAL2:31;
hence B in omega by A5, ORDINAL1:12; :: thesis: verum

end;

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