let a be Ordinal; :: thesis: a *^ a = exp (a,2)
consider fi being Ordinal-Sequence such that
A1: ( exp (a,2) = last fi & dom fi = succ 2 & fi . 0 = 1 ) and
A2: for c being Ordinal st succ c in succ 2 holds
fi . (succ c) = a *^ (fi . c) and
for c being Ordinal st c in succ 2 & c <> 0 & c is limit_ordinal holds
fi . c = lim (fi | c) by ORDINAL2:def 16;
( succ 0 in succ (succ 0) & succ (succ 0) in succ 2 ) by ORDINAL1:6;
then A3: ( succ 0 in succ 2 & succ (succ 0) in succ 2 ) by ORDINAL1:10;
exp (a,2) = fi . 2 by A1, ORDINAL2:6
.= a *^ (fi . (succ 0)) by A2, A3
.= a *^ (a *^ (fi . 0)) by A2, A3
.= a *^ a by A1, ORDINAL2:39 ;
hence a *^ a = exp (a,2) ; :: thesis: verum