∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : CompactSpace α]
  (f : C(α, β)), BoundedContinuousFunction.mkOfCompact (-f) = -BoundedContinuousFunction.mkOfCompact f