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