∀ {R : Type u} [inst : Ring R] [inst_1 : SizeOf R] (toTopologicalSpace : TopologicalSpace R)
  (toIsTopologicalRing : IsTopologicalRing R),
  sizeOf { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing } =
    1 + sizeOf toTopologicalSpace + sizeOf toIsTopologicalRing