I guess I should say what I've settled on doing.  Having re-written my notes _again_ I'm now using a version of the Exchange Lemma which is very close to that in the Wikipedia article.  Previously I'd been following [Kaye+Wilson][1] which builds this result up via a couple of lemmas.  I think the new version is sufficiently streamlined that I can do it, and then get onto big results, all in a lecture.

The approach which Robin, Andrew et al. suggest (that is, leverage what we already know about matrices) is attractive.  But I think it's too late for me this year (and we're re-writing all our syllabi at present, so the course will have to be seriously rethought next year or the one after anyway).  I also have a sneaking suspicion that a proof relying upon Gaussian Elimination will fail to convince nearly as many students as the Exchange Lemma version.

Thanks for all the responses: some very useful ideas!

  [1]: https://www.amazon.co.uk/Linear-Algebra-Oxford-Science-Publications/dp/0198502370