let x, y be object ; :: thesis: 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 ) )
let f be one-to-one Function; :: thesis: 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 ) )
let R be Relation; :: thesis: ( [x,y] in (f * R) * (f ") iff ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) )
A1: rng f = dom (f ") by FUNCT_1:33;
A2: dom f = rng (f ") by FUNCT_1:33;

hereby :: thesis: ( x in dom f & y in dom f & [(f . x),(f . y)] in R implies [x,y] in (f * R) * (f ") )

assume [x,y] in (f * R) * (f ") ; :: thesis: ( x in dom f & y in dom f & [(f . x),(f . y)] in R )
then consider a being object such that
A3: [x,a] in f * R and
A4: [a,y] in f " by RELAT_1:def 8;
A5: ( y = (f ") . a & a in rng f ) by A1, A4, FUNCT_1:1;
consider b being object such that
A6: [x,b] in f and
A7: [b,a] in R by A3, RELAT_1:def 8;
thus ( x in dom f & y in dom f ) by A2, A4, A6, XTUPLE_0:def 12, XTUPLE_0:def 13; :: thesis: [(f . x),(f . y)] in R
b = f . x by A6, FUNCT_1:1;
hence [(f . x),(f . y)] in R by A7, A5, FUNCT_1:35; :: thesis: verum

end;

assume that
A8: x in dom f and
A9: y in dom f and
A10: [(f . x),(f . y)] in R ; :: thesis: [x,y] in (f * R) * (f ")
( (f ") . (f . y) = y & f . y in rng f ) by A9, FUNCT_1:34, FUNCT_1:def 3;
then A11: [(f . y),y] in f " by A1, FUNCT_1:1;
[x,(f . x)] in f by A8, FUNCT_1:1;
then [x,(f . y)] in f * R by A10, RELAT_1:def 8;
hence [x,y] in (f * R) * (f ") by A11, RELAT_1:def 8; :: thesis: verum