let m, n be Nat; :: thesis: m |^|^ (n + 1) = m |^ (m |^|^ n)
succ (Segm n) = Segm (n + 1) by NAT_1:38;
hence m |^|^ (n + 1) = exp (m,(m |^|^ n)) by ORDINAL5:14
.= m |^ (m |^|^ n) ;
:: thesis: verum