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

A2: now

let b be ordinal number ; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume B1: S₁[b] ; :: thesis: S₁[ succ b]
B2: a |^|^ (succ b) = exp a,(a |^|^ b) by Th1;
B4: succ 0 = 0 + 1 ;
thus S₁[ succ b] :: thesis: verum

proof

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

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

then 1 c= a |^|^ b by B4, ORDINAL1:33, A0, B1;
then exp a,1 c= exp a,(a |^|^ b) by A0, ORDINAL4:27;
hence S₁[ succ b] by B2, ORDINAL2:63; :: thesis: verum

end;

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

then a |^|^ b = 1 by Th0;
hence S₁[ succ b] by B2, ORDINAL2:63; :: thesis: verum

end;

end;

end;

end;

A3: now

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 C1: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S₁[b] ) ) ; :: thesis: S₁[c]
deffunc H₁( Ordinal) -> Ordinal = a |^|^ $1;
consider phi being Ordinal-Sequence such that
C2: ( dom phi = c & ( for b being ordinal number st b in c holds
phi . b = H₁(b) ) ) from ORDINAL2:sch 3();
phi is non-decreasing

proof

let e be ordinal number ; :: according to ORDINAL5:def 2 :: thesis: for b being ordinal number st e in b & b in dom phi holds
phi . e c= phi . b
let b be ordinal number ; :: thesis: ( e in b & b in dom phi implies phi . e c= phi . b )
assume D1: ( e in b & b in dom phi ) ; :: thesis: phi . e c= phi . b
then D2: ( phi . b = H₁(b) & e in c ) by C2, ORDINAL1:19;
then ( phi . e = H₁(e) & e c= b ) by C2, D1, ORDINAL1:def 2;
hence phi . e c= phi . b by A0, D2, Th5; :: thesis: verum

end;

then C3: Union phi is_limes_of phi by C1, C2, ThND;
lim phi = H₁(c) by C1, C2, Th2;
then C4: H₁(c) = Union phi by C3, ORDINAL2:def 14;
thus S₁[c] :: thesis: verum

proof

assume 0 in c ; :: thesis: a c= a |^|^ c
then succ 0 in c by C1, ORDINAL1:41;
then ( phi . 1 in rng phi & phi . 1 = H₁(1) & H₁(1) = a ) by C2, Th3, FUNCT_1:def 5;
hence a c= a |^|^ c by C4, ZFMISC_1:92; :: thesis: verum

end;

end;

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