let x be set ; :: thesis: for U being non empty set
for f being Function
for R being total reflexive Relation of U st x in dom f & f is U -valued holds
f is id {x},R -respecting
let U be non empty set ; :: thesis: for f being Function
for R being total reflexive Relation of U st x in dom f & f is U -valued holds
f is id {x},R -respecting
let f be Function; :: thesis: for R being total reflexive Relation of U st x in dom f & f is U -valued holds
f is id {x},R -respecting
let R be total reflexive Relation of U; :: thesis: ( x in dom f & f is U -valued implies f is id {x},R -respecting )
set E = id {x};
assume A1: x in dom f ; :: thesis: ( not f is U -valued or f is id {x},R -respecting )
then reconsider D = dom f as non empty set ;
(id {x}) \+\ {[x,x]} = {} ;
then A2: id {x} = {[x,x]} by FOMODEL0:29;
reconsider xx = x as Element of D by A1;
assume f is U -valued ; :: thesis: f is id {x},R -respecting
then rng f c= U by RELAT_1:def 19;
then reconsider ff = f as Function of D,U by FUNCT_2:2;

now :: thesis: for x1, x2 being set st [x1,x2] in id {x} holds
[(f . x1),(f . x2)] in R

let x1, x2 be set ; :: thesis: ( [x1,x2] in id {x} implies [(f . x1),(f . x2)] in R )
assume [x1,x2] in id {x} ; :: thesis: [(f . x1),(f . x2)] in R
then [x1,x2] = [x,x] by A2, TARSKI:def 1;
then A3: ( x1 = x & x2 = x ) by XTUPLE_0:1;
( f . xx = f . xx & ff . xx in U ) ;
hence [(f . x1),(f . x2)] in R by EQREL_1:5, A3; :: thesis: verum

end;

hence f is id {x},R -respecting ; :: thesis: verum