∀ {R : Type u} {S : Type v} {S' : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : CommSemiring S']
  (f : R →+* S) (g : S →+* S') (x : PrimeSpectrum S'),
  PrimeSpectrum.comap (g.comp f) x = PrimeSpectrum.comap f (PrimeSpectrum.comap g x)