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 ;
consider b being object such that
A6: [x,b] in f and
A7: [b,a] in R by ;
thus ( x in dom f & y in dom f ) by ; :: thesis: [(f . x),(f . y)] in R
b = f . x by ;
hence [(f . x),(f . y)] in R by ; :: 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 ;
then A11: [(f . y),y] in f " by ;
[x,(f . x)] in f by ;
then [x,(f . y)] in f * R by ;
hence [x,y] in (f * R) * (f ") by ; :: thesis: verum