let a be Ordinal; :: thesis: a |^|^ 1 = a
0 + 1 = succ 0 ;
hence a |^|^ 1 = exp (a,(a |^|^ 0)) by Th14
.= exp (a,1) by Th13
.= a by ORDINAL2:46 ;
:: thesis: verum