let a, b be Ordinal; :: thesis: ( 0 in a & omega c= b implies a |^|^ b = a |^|^ omega )
assume A1: 0 in a ; :: thesis: ( not omega c= b or a |^|^ b = a |^|^ omega )
assume omega c= b ; :: thesis: a |^|^ b = a |^|^ omega
then A2: b = omega +^ (b -^ omega) by ORDINAL3:def 5;
defpred S1[ Ordinal] means a |^|^ (omega +^ $1) = a |^|^ omega;
A3: S1[ 0 ] by ORDINAL2:27;
A4: for c being Ordinal st S1[c] holds
S1[ succ c]
proof
let c be Ordinal; :: thesis: ( S1[c] implies S1[ succ c] )
assume S1[c] ; :: thesis: S1[ succ c]
then A5: exp (a,(a |^|^ (omega +^ c))) = a |^|^ omega by A1, Th31;
thus a |^|^ (omega +^ (succ c)) = a |^|^ (succ (omega +^ c)) by ORDINAL2:28
.= a |^|^ omega by A5, Th14 ; :: thesis: verum
end;
A6: for c being Ordinal st c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S1[b] ) holds
S1[c]
proof
let c be Ordinal; :: thesis: ( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S1[b] ) implies S1[c] )
assume A7: ( c <> 0 & c is limit_ordinal ) ; :: thesis: ( ex b being Ordinal st
( b in c & not S1[b] ) or S1[c] )
assume A8: for b being Ordinal st b in c holds
S1[b] ; :: thesis: S1[c]
deffunc H1( Ordinal) -> Ordinal = a |^|^ $1;
consider f being Ordinal-Sequence such that
A9: ( dom f = omega +^ c & ( for b being Ordinal st b in omega +^ c holds
f . b = H1(b) ) ) from ORDINAL2:sch 3();
 ( omega +^ c <> {} & omega +^ c is limit_ordinal ) by A7, ORDINAL3:26, ORDINAL3:29;
then A10: a |^|^ (omega +^ c) = lim f by A9, Th15;
now :: thesis: ( a |^|^ omega <> {} & ( for B, C being Ordinal st B in a |^|^ omega & a |^|^ omega in C holds
ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) ) ) )
a c= a |^|^ omega by A1, Th23;
hence a |^|^ omega <> {} by A1; :: thesis: for B, C being Ordinal st B in a |^|^ omega & a |^|^ omega in C holds
ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )
let B, C be Ordinal; :: thesis: ( B in a |^|^ omega & a |^|^ omega in C implies ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) ) )
assume A11: ( B in a |^|^ omega & a |^|^ omega in C ) ; :: thesis: ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )
take D = omega ; :: thesis: ( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )
( omega +^ {} = omega & {} in c ) by A7, ORDINAL2:27, ORDINAL3:8;
hence D in dom f by A9, ORDINAL2:32; :: thesis: for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C )
let E be Ordinal; :: thesis: ( D c= E & E in dom f implies ( B in f . E & f . E in C ) )
assume A12: ( D c= E & E in dom f ) ; :: thesis: ( B in f . E & f . E in C )
then E -^ D in (omega +^ c) -^ omega by A9, ORDINAL3:53;
then E -^ D in c by ORDINAL3:52;
then S1[E -^ D] by A8;
then a |^|^ omega = a |^|^ E by A12, ORDINAL3:def 5;
hence ( B in f . E & f . E in C ) by A9, A11, A12; :: thesis: verum
end;
then a |^|^ omega is_limes_of f by ORDINAL2:def 9;
hence S1[c] by A10, ORDINAL2:def 10; :: thesis: verum
end;
for c being Ordinal holds S1[c] from ORDINAL2:sch 1(A3, A4, A6);
 hence a |^|^ b = a |^|^ omega by A2; :: thesis: verum