[isabelle] Let's find a proof of a lemma

Let's find a proof of the following lemma, which is forgotten in ZF theory:

lemma right_comp_id_any: "r<=Sigma(A,B) ==> r O id(C) = restrict(r,C)"

I think I can, spending some time, find a proof myself, but I suspect my proof won't be optimal.

Note that you have asked me to not send anymore missing lemmas in ZF. But this my message serves a different purpose, not to suggest its addition to ZF but to ask to help to find an elegant proof. (If you'll ask to not send messages like this, this will be the last.)

Victor Porton - http://portonvictor.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.