"Follows" in the sense that it is not an axiom - it has a proof of more than one line in the sense of the Hilbert system. Seeing functions as collections of ordered pairs tells us nothing here.

Your definition of ^ doesn't directly tell me that 2^1=2. It does tell me however that 0^0=1.