let a, b be Ordinal; :: thesis: a |^|^ (succ b) = exp (a,(a |^|^ b))
deffunc H₁( Ordinal) -> Ordinal = a |^|^ $1;
deffunc H₂( Ordinal, Ordinal-Sequence) -> set = lim $2;
deffunc H₃( Ordinal, Ordinal) -> set = exp (a,$2);
A1: for b, c being Ordinal holds
( c = H₁(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . 0 = 1 & ( for c being Ordinal st succ c in succ b holds
fi . (succ c) = H₃(c,fi . c) ) & ( for c being Ordinal st c in succ b & c <> 0 & c is limit_ordinal holds
fi . c = H₂(c,fi | c) ) ) ) by Def4;
for b being Ordinal holds H₁( succ b) = H₃(b,H₁(b)) from ORDINAL2:sch 15(A1);
hence a |^|^ (succ b) = exp (a,(a |^|^ b)) ; :: thesis: verum