>>331
> well-defined であるか？

sup なり inf なりがいつ存在するかがわかっていれば、ほぼ自明でしょ。

>>332
> ln は exp の逆関数であり、 expは級数で定義する。

そのほうが綺麗に導入できることは認めるけど、
初等関数 a^x を定義するのにそんな手間をかけるのはある意味馬鹿げてるともいえる。
つまり

> exp がwell-definedであり連続関数であり逆関数を持ち指数法則を満たすことは証明しないといけない。

なんてことを示してから、それでもってやっとこさ a^x が定義できる、というのはね。