theorem :: GROUP_9:120

for P, R being Relation holds
( P = (rng P) |` R iff P ~ = (R ~) | (dom (P ~)) ) by Lm35;