Dear Prof. Waddler, I don't know if the following proof is correct, please, let me know if I made any mistake: By hypothesis there exists k:S->T and h:k(S)->S such that h(k(S)) =_S s for all s in S and s =_S s' implies k(s) =_T k(s') for all s, s' in S On the other hand, there exists f:T->S and g:f(T)->S such that g(f(t)) =_T t for all t in T and t=_T t' implies f(t) =_S f(t') for all t, t' in T Assume that there exists t in T\k(S) => |T| > |S| because k is injective and S = dom(k). Hence, there exists t' not equal to t such that f(t) =_S f(t') which is absurdum. So, there not exists t in T\k(S), then T = k(S). So, k and k^-1 constitutes an equational correspondence. Yours, Alejandro -- Alejandro Díaz-Caro Homepage: http://www.fceia.unr.edu.ar/~diazcaro Weblog: http://computacioncuantica.exactas.org