let a be ordinal number ; :: thesis: a |^|^ 2 = exp (a,a)
2 = succ 1 ;
hence a |^|^ 2 = exp (a,(a |^|^ 1)) by Th1
.= exp (a,a) by Th3 ;
:: thesis: verum