I have a more general question about this, but thought I'd use a specific example instead.

I was trying to prove the Second Iso. Theorem for groups. Say G is a group and N a normal subgroup. I define the function f from {subgroups of G/N} to {subgroups of G containing N} by

.

I know this is well-defined but I would like to prove it. I know in general you take two elements in the domain, suppose they are equal and try to derive their image is equal. Then let

.

Then you can identify cosets on the left with cosets on the right, so . This only tells me that is in N. What do I do with this information? Should I do it some other way?

Am I over-estimating the fact its well defined-ness is not obvious? I know in general the question of well-defined comes up if, for example in equivalence classes, there is ambiguity of representative. Here there doesn't really seem to be such a problem, right? I don't know, I recently started to realise I should question whether functions I construct are well-defined or not, but I don't know when it's necessary to so or when it's obvious it is.