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