let x, y be set ; :: 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: ( dom f = rng (f " ) & rng f = dom (f " ) ) by FUNCT_1:55;

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 set such that
A2: ( [x,a] in f * R & [a,y] in f " ) by RELAT_1:def 8;
consider b being set such that
A3: ( [x,b] in f & [b,a] in R ) by A2, RELAT_1:def 8;
thus ( x in dom f & y in dom f ) by A1, A2, A3, RELAT_1:def 4, RELAT_1:def 5; :: thesis: [(f . x),(f . y)] in R
( b = f . x & y = (f " ) . a & a in rng f ) by A1, A2, A3, FUNCT_1:8;
hence [(f . x),(f . y)] in R by A3, FUNCT_1:57; :: thesis: verum

end;

assume A4: ( x in dom f & y in dom f & [(f . x),(f . y)] in R ) ; :: thesis: [x,y] in (f * R) * (f " )
then ( [x,(f . x)] in f & (f " ) . (f . y) = y & f . y in rng f ) by FUNCT_1:8, FUNCT_1:56, FUNCT_1:def 5;
then ( [x,(f . y)] in f * R & [(f . y),y] in f " ) by A1, A4, FUNCT_1:8, RELAT_1:def 8;
hence [x,y] in (f * R) * (f " ) by RELAT_1:def 8; :: thesis: verum