let a, b, c be Ordinal; :: 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:21;
then A3: ( 1 c< c or 1 = c ) ;

per cases ( c = 1 or 1 in c ) by A3, ORDINAL1:11;

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

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

end;

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

defpred S₁[ Ordinal] means for a, b being Ordinal st a c= b & b c= $1 holds
c |^|^ a c= c |^|^ b;
A5: S₁[ 0 ]

proof

let a, b be Ordinal; :: thesis: ( a c= b & b c= 0 implies c |^|^ a c= c |^|^ b )
assume A6: ( a c= b & b c= 0 ) ; :: thesis: c |^|^ a c= c |^|^ b
then b = {} ;
hence c |^|^ a c= c |^|^ b by A6; :: thesis: verum

end;

A7: now :: thesis: for d being Ordinal st S₁[d] holds
S₁[ succ d]

let d be Ordinal; :: thesis: ( S₁[d] implies S₁[ succ d] )
assume A8: S₁[d] ; :: thesis: S₁[ succ d]
c |^|^ (succ d) = exp (c,(c |^|^ d)) by Th14;
then A9: c |^|^ d c= c |^|^ (succ d) by A4, ORDINAL4:32;
thus S₁[ succ d] :: thesis: verum

proof

let a, b be Ordinal; :: thesis: ( a c= b & b c= succ d implies c |^|^ a c= c |^|^ b )
assume A10: ( a c= b & b c= succ d ) ; :: thesis: c |^|^ a c= c |^|^ b
A11: a c= succ d by A10;

per cases ( b c= d or ( b = succ d & a = succ d ) or ( b = succ d & a c= d ) ) by A10, A11, Th1;

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

hence c |^|^ a c= c |^|^ b by A8, A10; :: 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 A12: ( b = succ d & a c= d ) ; :: thesis: c |^|^ a c= c |^|^ b

then c |^|^ a c= c |^|^ d by A8;
hence c |^|^ a c= c |^|^ b by A9, A12; :: thesis: verum

end;

end;

end;

end;

A13: now :: thesis: for d being Ordinal st d <> 0 & d is limit_ordinal & ( for e being Ordinal st e in d holds
S₁[e] ) holds
S₁[d]

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

proof

let a be Ordinal; :: according to ORDINAL5:def 2 :: thesis: for b being Ordinal st a in b & b in dom f holds
f . a c= f . b
let b be Ordinal; :: thesis: ( a in b & b in dom f implies f . a c= f . b )
assume A17: ( a in b & b in dom f ) ; :: thesis: f . a c= f . b
then ( a c= b & S₁[b] ) by A15, A16, ORDINAL1:def 2;
then ( c |^|^ a c= c |^|^ b & a in d & f . b = H₁(b) ) by A16, A17, ORDINAL1:12;
hence f . a c= f . b by A16; :: thesis: verum

end;

then A18: Union f is_limes_of f by A14, A16, Th6;
c |^|^ d = lim f by A14, A16, Th15;
then A19: c |^|^ d = Union f by A18, ORDINAL2:def 10;
thus S₁[d] :: thesis: verum

proof

let a, b be Ordinal; :: thesis: ( a c= b & b c= d implies c |^|^ a c= c |^|^ b )
assume A20: ( a c= b & b c= d ) ; :: thesis: c |^|^ a c= c |^|^ b
then A21: ( ( b c< d or b = d ) & ( a c< b or a = b ) ) ;

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

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

hence H₁(a) c= H₁(b) by A20, A15; :: thesis: verum

end;

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

then ( f . a in rng f & f . a = H₁(a) ) by A16, FUNCT_1:def 3;
hence H₁(a) c= H₁(b) by A19, A22, ZFMISC_1:74; :: 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 holds S₁[b] from ORDINAL2:sch 1(A5, A7, A13);
hence c |^|^ a c= c |^|^ b by A1; :: thesis: verum

end;

end;