∀ {α : Type u_1} {γ : Type u_2} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_1 : TopologicalSpace α]
  [inst_2 : BorelSpace α] [inst_3 : TopologicalSpace γ] [inst_4 : TopologicalSpace.PseudoMetrizableSpace γ]
  [inst_5 : AddCommGroup γ] [inst_6 : IsTopologicalAddGroup γ] [inst_7 : SecondCountableTopologyEither α γ]
  (x y : C(α, γ)),
  (↑(ContinuousMap.toAEEqFunAddHom μ)).toFun (x + y) =
    (↑(ContinuousMap.toAEEqFunAddHom μ)).toFun x + (↑(ContinuousMap.toAEEqFunAddHom μ)).toFun y