∀ {M : Type u_3} [inst : MulOneClass M] [inst_1 : SizeOf M] (toSubsemigroup : Subsemigroup M)
  (one_mem' : 1 ∈ toSubsemigroup.carrier),
  sizeOf { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = 1 + sizeOf toSubsemigroup + sizeOf one_mem'