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