There is another (messy) proof of uniqueness in Grillet, Abstract algebra, which I don't like. The proof here is a shortcut I thought up. --barto (talk) (contribs) 18:00, 13 January 2018 (EST)