Classical capacity of memoryless classical channels

import 

theorem capacity_of_memoryless (W : channel) [memoryless W] :
  capacity W  = Sup { i : ℝ | ∃ rnd_var X, I(X;W(X)) = i } :=
sorry