let a, b be Ordinal; :: thesis:
assume A1: ( 0 in a & 0 in b ) ; :: thesis:
defpred S₁[ Ordinal] means ( 0 in $1 implies a c= a |^|^ $1 );
A2: S₁[ 0 ] ;

A3: now :: thesis:

let b be Ordinal; :: thesis:
assume A4: S₁[b] ; :: thesis:
A5: a |^|^ (succ b) = exp (a,(a |^|^ b)) by Th14;
A6: succ 0 = 0 + 1 ;
thus S₁[ succ b] :: thesis:

proof

per cases by ORDINAL3:8;

suppose 0 in b ; :: thesis:

then 1 c= a |^|^ b by A6, A1, A4, ORDINAL1:21;
then exp (a,1) c= exp (a,(a |^|^ b)) by A1, ORDINAL4:27;
hence S₁[ succ b] by A5, ORDINAL2:46; :: thesis:

end;

suppose b = 0 ; :: thesis:

then a |^|^ b = 1 by Th13;
hence S₁[ succ b] by A5, ORDINAL2:46; :: thesis:

end;

end;

end;

end;

A7: now :: thesis:

let c be Ordinal; :: thesis:
assume A8: ( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S₁[b] ) ) ; :: thesis:
deffunc H₁( Ordinal) -> Ordinal = a |^|^ $1;
consider phi being Ordinal-Sequence such that
A9: ( dom phi = c & ( for b being Ordinal st b in c holds
phi . b = H₁(b) ) ) from ORDINAL2:sch 3();
phi is non-decreasing

proof

let e be Ordinal; :: according to ORDINAL5:def 2 :: thesis:
let b be Ordinal; :: thesis:
assume A10: ( e in b & b in dom phi ) ; :: thesis:
then A11: ( phi . b = H₁(b) & e in c ) by A9, ORDINAL1:10;
then ( phi . e = H₁(e) & e c= b ) by A9, A10, ORDINAL1:def 2;
hence phi . e c= phi . b by A1, A11, Th21; :: thesis:

end;

then A12: Union phi is_limes_of phi by A8, A9, Th6;
lim phi = H₁(c) by A8, A9, Th15;
then A13: H₁(c) = Union phi by A12, ORDINAL2:def 10;
thus S₁[c] :: thesis:

proof

assume 0 in c ; :: thesis:
then succ 0 in c by A8, ORDINAL1:28;
then ( phi . 1 in rng phi & phi . 1 = H₁(1) & H₁(1) = a ) by A9, Th16, FUNCT_1:def 3;
hence a c= a |^|^ c by A13, ZFMISC_1:74; :: thesis:

end;

end;

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