let a, b, c be ordinal number ; :: thesis: ( a c= b & 0 in c implies c |^|^ a c= c |^|^ b )
assume that
A1: a c= b and
A2: 0 in c ; :: thesis: c |^|^ a c= c |^|^ b
( succ 0 c= c & succ 0 = 0 + 1 ) by A2, ORDINAL1:33;
then AA: ( 1 c< c or 1 = c ) by XBOOLE_0:def 8;

per cases ( c = 1 or 1 in c ) by AA, ORDINAL1:21;

suppose c = 1 ; :: thesis: c |^|^ a c= c |^|^ b

then ( c |^|^ a = 1 & c |^|^ b = 1 ) by Th4;
hence c |^|^ a c= c |^|^ b ; :: thesis: verum

end;

suppose A0: 1 in c ; :: thesis: c |^|^ a c= c |^|^ b

defpred S₁[ Ordinal] means for a, b being ordinal number st a c= b & b c= $1 holds
c |^|^ a c= c |^|^ b;
P0: S₁[ {} ]

proof

let a, b be ordinal number ; :: thesis: ( a c= b & b c= {} implies c |^|^ a c= c |^|^ b )
assume B0: ( a c= b & b c= {} ) ; :: thesis: c |^|^ a c= c |^|^ b
then b = {} by XBOOLE_1:3;
hence c |^|^ a c= c |^|^ b by B0, XBOOLE_1:3; :: thesis: verum

end;

P1: now

let d be ordinal number ; :: thesis: ( S₁[d] implies S₁[ succ d] )
assume A3: S₁[d] ; :: thesis: S₁[ succ d]
c |^|^ (succ d) = exp (c,(c |^|^ d)) by Th1;
then A6: c |^|^ d c= c |^|^ (succ d) by A0, ORDINAL4:32;
thus S₁[ succ d] :: thesis: verum

proof

let a, b be ordinal number ; :: thesis: ( a c= b & b c= succ d implies c |^|^ a c= c |^|^ b )
assume A4: ( a c= b & b c= succ d ) ; :: thesis: c |^|^ a c= c |^|^ b
A5: a c= succ d by A4, XBOOLE_1:1;

per cases ( b c= d or ( b = succ d & a = succ d ) or ( b = succ d & a c= d ) ) by A4, A5, Th001;

suppose b c= d ; :: thesis: c |^|^ a c= c |^|^ b

hence c |^|^ a c= c |^|^ b by A3, A4; :: thesis: verum

end;

suppose ( b = succ d & a = succ d ) ; :: thesis: c |^|^ a c= c |^|^ b

hence c |^|^ a c= c |^|^ b ; :: thesis: verum

end;

suppose A7: ( b = succ d & a c= d ) ; :: thesis: c |^|^ a c= c |^|^ b

then c |^|^ a c= c |^|^ d by A3;
hence c |^|^ a c= c |^|^ b by A6, A7, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

end;

P2: now

let d be ordinal number ; :: thesis: ( d <> {} & d is limit_ordinal & ( for e being ordinal number st e in d holds
S₁[e] ) implies S₁[d] )
assume that
B1: ( d <> {} & d is limit_ordinal ) and
B2: for e being ordinal number st e in d holds
S₁[e] ; :: thesis: S₁[d]
deffunc H₁( Ordinal) -> Ordinal = c |^|^ $1;
consider f being Ordinal-Sequence such that
B3: ( dom f = d & ( for e being ordinal number st e in d holds
f . e = H₁(e) ) ) from ORDINAL2:sch 3();
f is non-decreasing

proof

let a be ordinal number ; :: according to ORDINAL5:def 2 :: thesis: for b being ordinal number st a in b & b in dom f holds
f . a c= f . b
let b be ordinal number ; :: thesis: ( a in b & b in dom f implies f . a c= f . b )
assume C0: ( a in b & b in dom f ) ; :: thesis: f . a c= f . b
then ( a c= b & S₁[b] ) by B2, B3, ORDINAL1:def 2;
then ( c |^|^ a c= c |^|^ b & a in d & f . b = H₁(b) ) by B3, C0, ORDINAL1:22;
hence f . a c= f . b by B3; :: thesis: verum

end;

then B4: Union f is_limes_of f by B1, B3, ThND;
c |^|^ d = lim f by B1, B3, Th2;
then B5: c |^|^ d = Union f by B4, ORDINAL2:def 14;
thus S₁[d] :: thesis: verum

proof

let a, b be ordinal number ; :: thesis: ( a c= b & b c= d implies c |^|^ a c= c |^|^ b )
assume C1: ( a c= b & b c= d ) ; :: thesis: c |^|^ a c= c |^|^ b
then C2: ( ( b c< d or b = d ) & ( a c< b or a = b ) ) by XBOOLE_0:def 8;

per cases ( b in d or ( b = d & a in d ) or ( b = d & a = d ) ) by C2, ORDINAL1:21;

suppose b in d ; :: thesis: c |^|^ a c= c |^|^ b

hence H₁(a) c= H₁(b) by C1, B2; :: thesis: verum

end;

suppose C3: ( b = d & a in d ) ; :: thesis: c |^|^ a c= c |^|^ b

then ( f . a in rng f & f . a = H₁(a) ) by B3, FUNCT_1:def 5;
hence H₁(a) c= H₁(b) by B5, C3, ZFMISC_1:92; :: thesis: verum

end;

suppose ( b = d & a = d ) ; :: thesis: c |^|^ a c= c |^|^ b

hence H₁(a) c= H₁(b) ; :: thesis: verum

end;

end;

end;

end;

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

end;

end;