let x be set ; :: 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 " ) )
assume x in field ((f * R) * (f " )) ; :: thesis: [x,x] in (f * R) * (f " )
then A1: x in (dom ((f * R) * (f " ))) \/ (rng ((f * R) * (f " ))) by RELAT_1:def 6;
A2: R is_reflexive_in field R by RELAT_2:def 9;

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

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

then consider y being set such that
A3: [x,y] in (f * R) * (f " ) by RELAT_1:def 4;
A4: ( x in dom f & [(f . x),(f . y)] in R ) by A3, Th6;
then f . x in field R by RELAT_1:30;
then [(f . x),(f . x)] in R by A2, RELAT_2:def 1;
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 set such that
A5: [y,x] in (f * R) * (f " ) by RELAT_1:def 5;
A6: ( x in dom f & [(f . y),(f . x)] in R ) by A5, Th6;
then f . x in field R by RELAT_1:30;
then [(f . x),(f . x)] in R by A2, RELAT_2:def 1;
hence [x,x] in (f * R) * (f " ) by A6, Th6; :: thesis: verum

end;

end;