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;

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

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;

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;

end;