Proving that DFA equivalence is decidable
Here is a slightly different proof, along similar lines.

Lemma 1. Let $A$ be a DFA having $n$ states, and let $B$ be a DFA having $m$ states. There is a DFA $C$ having $nm$ states such that $L(C) = [L(A) \setminus L(B)] \cup [L(B) \setminus L(A)]$.

The proof uses the product construction (exercise).

Lemma 2. Let $C$ be a DFA having $p$ states. If $L(C) \neq \emptyset$ then $L(C)$ contains some word of length at most $p-1$.

Proof sketch. The language $L(C)$ is non-empty if some final state $q_f$ is reachable from the initial state $q_0$. The shortest path from $q_0$ to $q_f$ has length at most $p-1$, and this corresponds to a word of length at most $p-1$ in $L(C)$.

Theorem. Let $A$ be a DFA having $n$ states, and let $B$ be a DFA having $m$ states. Then $L(A) = L(B)$ iff for all words $w$ of length at most $nm-1$, either $w \in L(A),L(B)$ or $w \notin L(A),L(B)$.

Proof. If $L(A) = L(B)$ then the condition clearly holds. If $L(A) \neq L(B)$ then $\Delta := [L(A) \setminus L(B)] \cup [L(B) \setminus L(A)] \neq \emptyset$. According to Lemma 1, there is a DFA having $nm$ states whose language is $\Delta \neq \emptyset$. According to Lemma 2 (with $p = nm$), there exists a word $w \in \Delta$ of length at most $nm-1$. This is a word for which it doesn't hold that either $w \in L(A),L(B)$ or $w \notin L(A),L(B)$.