let a, b be ordinal number ; :: thesis: ( 0 in a & omega c= b implies a |^|^ b = a |^|^ omega )
assume Z0: 0 in a ; :: thesis: ( not omega c= b or a |^|^ b = a |^|^ omega )
assume omega c= b ; :: thesis: a |^|^ b = a |^|^ omega
then Z1: b = omega +^ (b -^ omega ) by ORDINAL3:def 6;
defpred S₁[ Ordinal] means a |^|^ (omega +^ $1) = a |^|^ omega ;
A0: S₁[ {} ] by ORDINAL2:44;
A1: for c being ordinal number st S₁[c] holds
S₁[ succ c]

proof

let c be ordinal number ; :: thesis: ( S₁[c] implies S₁[ succ c] )
assume S₁[c] ; :: thesis: S₁[ succ c]
then B1: exp a,(a |^|^ (omega +^ c)) = a |^|^ omega by Z0, Th12;
thus a |^|^ (omega +^ (succ c)) = a |^|^ (succ (omega +^ c)) by ORDINAL2:45
.= a |^|^ omega by B1, Th1 ; :: thesis: verum

end;

A2: for c being ordinal number st c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S₁[b] ) holds
S₁[c]

proof

let c be ordinal number ; :: thesis: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S₁[b] ) implies S₁[c] )
assume Z2: ( c <> {} & c is limit_ordinal ) ; :: thesis: ( ex b being ordinal number st
( b in c & not S₁[b] ) or S₁[c] )
assume Z3: for b being ordinal number st b in c holds
S₁[b] ; :: thesis: S₁[c]
deffunc H₁( Ordinal) -> Ordinal = a |^|^ $1;
consider f being Ordinal-Sequence such that
A3: ( dom f = omega +^ c & ( for b being ordinal number st b in omega +^ c holds
f . b = H₁(b) ) ) from ORDINAL2:sch 3();
( omega +^ c <> {} & omega +^ c is limit_ordinal ) by Z2, ORDINAL3:29, ORDINAL3:32;
then A5: a |^|^ (omega +^ c) = lim f by A3, Th2;

now

a c= a |^|^ omega by Z0, Th6;
hence a |^|^ omega <> {} by Z0; :: 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 A7: ( 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 Z2, ORDINAL2:44, ORDINAL3:10;
hence D in dom f by A3, ORDINAL2:49; :: 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 A6: ( D c= E & E in dom f ) ; :: thesis: ( B in f . E & f . E in C )
then E -^ D in (omega +^ c) -^ omega by A3, ORDINAL3:66;
then E -^ D in c by ORDINAL3:65;
then S₁[E -^ D] by Z3;
then a |^|^ omega = a |^|^ E by A6, ORDINAL3:def 6;
hence ( B in f . E & f . E in C ) by A3, A7, A6; :: thesis: verum

end;

then a |^|^ omega is_limes_of f by ORDINAL2:def 13;
hence S₁[c] by A5, ORDINAL2:def 14; :: thesis: verum

end;

for c being ordinal number holds S₁[c] from ORDINAL2:sch 1(A0, A1, A2);
hence a |^|^ b = a |^|^ omega by Z1; :: thesis: verum