Proved the second lemma in the section on finite geochars. It need polishing later.

That's all for tonight. Moving on to the section on restriction to the
identity component tomorrow.