let a be Ordinal; :: thesis: a |^|^ 2 = exp (a,a)
2 = succ 1 ;
hence a |^|^ 2 = exp (a,(a |^|^ 1)) by Th14
.= exp (a,a) by Th16 ;
:: thesis: verum