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 S₁[ Ordinal] means a |^|^ (omega +^ $1) = a |^|^ omega;
A3: S₁[ 0 ] by ORDINAL2:27;
A4: for c being Ordinal st S₁[c] holds
S₁[ succ c]

proof

let c be Ordinal; :: thesis: ( S₁[c] implies S₁[ succ c] )
assume S₁[c] ; :: thesis: S₁[ 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
S₁[b] ) holds
S₁[c]

proof

let c be Ordinal; :: thesis: ( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S₁[b] ) implies S₁[c] )
assume A7: ( c <> 0 & c is limit_ordinal ) ; :: thesis: ( ex b being Ordinal st
( b in c & not S₁[b] ) or S₁[c] )
assume A8: for b being Ordinal st b in c holds
S₁[b] ; :: thesis: S₁[c]
deffunc H₁( 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 = H₁(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 S₁[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 S₁[c] by A10, ORDINAL2:def 10; :: thesis: verum

end;

for c being Ordinal holds S₁[c] from ORDINAL2:sch 1(A3, A4, A6);
hence a |^|^ b = a |^|^ omega by A2; :: thesis: verum