let a be ordinal number ; :: thesis: a |^|^ 1 = a
0 + 1 = succ 0 ;
hence a |^|^ 1 = exp (a,(a |^|^ 0)) by Th1
.= exp (a,1) by Th0
.= a by ORDINAL2:63 ;
:: thesis: verum