let x be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not x in field ((f * R) * (f ")) or [x,x] in (f * R) * (f ") )

A1: R is_reflexive_in field R by RELAT_2:def 9;

assume x in field ((f * R) * (f ")) ; :: thesis: [x,x] in (f * R) * (f ")

then A2: x in (dom ((f * R) * (f "))) \/ (rng ((f * R) * (f "))) by RELAT_1:def 6;

A1: R is_reflexive_in field R by RELAT_2:def 9;

assume x in field ((f * R) * (f ")) ; :: thesis: [x,x] in (f * R) * (f ")

then A2: x in (dom ((f * R) * (f "))) \/ (rng ((f * R) * (f "))) by RELAT_1:def 6;

per cases
( x in dom ((f * R) * (f ")) or x in rng ((f * R) * (f ")) )
by A2, XBOOLE_0:def 3;

end;

suppose
x in dom ((f * R) * (f "))
; :: thesis: [x,x] in (f * R) * (f ")

then consider y being object such that

A3: [x,y] in (f * R) * (f ") by XTUPLE_0:def 12;

[(f . x),(f . y)] in R by A3, Th6;

then f . x in field R by RELAT_1:15;

then A4: [(f . x),(f . x)] in R by A1;

x in dom f by A3, Th6;

hence [x,x] in (f * R) * (f ") by A4, Th6; :: thesis: verum

end;A3: [x,y] in (f * R) * (f ") by XTUPLE_0:def 12;

[(f . x),(f . y)] in R by A3, Th6;

then f . x in field R by RELAT_1:15;

then A4: [(f . x),(f . x)] in R by A1;

x in dom f by A3, Th6;

hence [x,x] in (f * R) * (f ") by A4, Th6; :: thesis: verum

suppose
x in rng ((f * R) * (f "))
; :: thesis: [x,x] in (f * R) * (f ")

then consider y being object such that

A5: [y,x] in (f * R) * (f ") by XTUPLE_0:def 13;

[(f . y),(f . x)] in R by A5, Th6;

then f . x in field R by RELAT_1:15;

then A6: [(f . x),(f . x)] in R by A1;

x in dom f by A5, Th6;

hence [x,x] in (f * R) * (f ") by A6, Th6; :: thesis: verum

end;A5: [y,x] in (f * R) * (f ") by XTUPLE_0:def 13;

[(f . y),(f . x)] in R by A5, Th6;

then f . x in field R by RELAT_1:15;

then A6: [(f . x),(f . x)] in R by A1;

x in dom f by A5, Th6;

hence [x,x] in (f * R) * (f ") by A6, Th6; :: thesis: verum