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;

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

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 that 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;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

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