Addition of exponents proof in group theory

Mr Davis 97
Just out of curiosity, what would a proof of ##a^m a^n = a^{m+n}## amount to? Of course obviously if you have n of one thing and m of another you get m+n, but I am wondering if this is rigorous enough, or if you need induction.

Mentor
2021 Award
Formally you need a prove by induction, because this notation is an abbreviation, or a conclusion from the special to the general (forgotten the formal name). But the essential part is the use of the associative law, which is needed to allow this abbreviation in the first place.

It looks to me that $$a^m=a\times a\times a .....$$ (m terms) by definition. So $$a^m \times a^n =a^{m+n}$$ from the definition. I don't think associative law is needed.

Mentor
2021 Award
It looks to me that $$a^m=a\times a\times a .....$$ (m terms) by definition. So $$a^m \times a^n =a^{m+n}$$ from the definition. I don't think associative law is needed.
##a \cdot a \cdot a## isn't defined without associativity. And what if ##a \cdot b \neq b \cdot a## with ##b=a^2\,##? Of course this doesn't happen in a group, because of associativity. But it cannot be ruled out for an algebra.

Mr Davis 97
Formally you need a prove by induction, because this notation is an abbreviation, or a conclusion from the special to the general (forgotten the formal name). But the essential part is the use of the associative law, which is needed to allow this abbreviation in the first place.
Okay. Well given that I understand that the associative law will have to be used, how do I in general go about doing an induction when there are two variables m and n instead of just n?

Mentor
2021 Award
You could do a double induction, a nested argument. But as this entire formula comes down, to what ##a^n## actually means, I think it will do to say: Let ##n,m## be arbitrary natural (integer) numbers, then ##a^n## means ... To set up an entire induction is really a bit of over munitioned.