Fix a lemma

The statement of lemma-w-local-algebraic-residue-field-extensions
was wrong. Fixed and now there is a proof as well.