>However, I think there is
>a step that seems
>suspect, that is:
>
>x*(y+z) + x = (x*y + x*z) + x
>
>That step looks like it uses
>the very thing which is
>being proven here. Is it
>so, or am I overlooking
>something rather trivial?

Yes. The proof of the distributive law is by induction in z.
Just before that derivation I say, "Let M be the set of all z for which the Law holds. We just saw that, by Definition 2, 1 is in M. Let z be in M. Then ..."

At this point we do not know yet whether the law holds universaly, but do know that it holds for 1 and have assumed that it also holds for z - a specific but arbitrary number, which means that

x*(y+z) = x*y + x*z

by our assumption. From here it follows, as the derivation you pointed to shows, that

x*(y+z') = x*y + x*z'

and, by induction, it holds for all numbers.

>Currently, I'm a third-year student of
>theoretical physics in university, so
>I think I should know
>enough to understand this.

That's OK. I think I should have mentioned that the proof is by induction. Sorry.