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

A3: now :: thesis: for b being Ordinal st S₁[b] holds
S₁[ succ b]

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

proof

per cases ( 0 in b or b = 0 ) by ORDINAL3:8;

suppose 0 in b ; :: thesis: S₁[ succ b]

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: verum

end;

suppose b = 0 ; :: thesis: S₁[ succ b]

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

end;

end;

end;

end;

A7: now :: thesis: 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]

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 A8: ( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S₁[b] ) ) ; :: thesis: S₁[c]
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: for b being Ordinal st e in b & b in dom phi holds
phi . e c= phi . b
let b be Ordinal; :: thesis: ( e in b & b in dom phi implies phi . e c= phi . b )
assume A10: ( e in b & b in dom phi ) ; :: thesis: phi . e c= phi . b
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: verum

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: verum

proof

assume 0 in c ; :: thesis: a c= a |^|^ c
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: verum

end;

end;

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