∀ {G : Type u_6} {inst : AddGroup G} {toFun : G → ℝ} {map_zero' : toFun 0 = 0}
  {add_le' : ∀ (r s : G), toFun (r + s) ≤ toFun r + toFun s} {neg' : ∀ (r : G), toFun (-r) = toFun r} {toFun_1 : G → ℝ}
  {map_zero'_1 : toFun_1 0 = 0} {add_le'_1 : ∀ (r s : G), toFun_1 (r + s) ≤ toFun_1 r + toFun_1 s}
  {neg'_1 : ∀ (r : G), toFun_1 (-r) = toFun_1 r},
  { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' } =
      { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 } →
    toFun = toFun_1