let x, y be 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 ) )
let f be 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 R be Relation; ( [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 ( 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 ")
;
( 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;
[(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;
verum
end;
assume that
A8:
x in dom f
and
A9:
y in dom f
and
A10:
[(f . x),(f . y)] in R
; [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; verum