∀ {M : Type u_1} [inst : Add M] {N : Type u_2} [inst_1 : Add N] {S : Set M} {T : Set N},
  S.Nonempty →
    T.Nonempty →
      ∀ (x : M × N),
        (∀ (a : M) (b : N), a ∈ S ∧ b ∈ T → (a + x.1, b + x.2) = (x.1 + a, x.2 + b)) ↔
          (∀ m ∈ S, m + x.1 = x.1 + m) ∧ ∀ m ∈ T, m + x.2 = x.2 + m