theorem Th6: :: YELLOW21:6

for x, y being object
for f being one-to-one Function
for R being Relation holds
( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )