let X, x be set ; :: thesis: for U being non empty set
for R being total reflexive Relation of U
for f being Function of X,U st x in X holds
f is {[x,x]},R -respecting
let U be non empty set ; :: thesis: for R being total reflexive Relation of U
for f being Function of X,U st x in X holds
f is {[x,x]},R -respecting
let R be total reflexive Relation of U; :: thesis: for f being Function of X,U st x in X holds
f is {[x,x]},R -respecting
let f be Function of X,U; :: thesis: ( x in X implies f is {[x,x]},R -respecting )
reconsider E = {[x,x]} as Relation ;
assume A1: x in X ; :: thesis: f is {[x,x]},R -respecting
then reconsider XX = X as non empty set ;
reconsider ff = f as Function of XX,U ;

now :: thesis: for x1, x2 being set st [x1,x2] in E holds
[(f . x1),(f . x2)] in R

let x1, x2 be set ; :: thesis: ( [x1,x2] in E implies [(f . x1),(f . x2)] in R )
assume [x1,x2] in E ; :: thesis: [(f . x1),(f . x2)] in R
then A2: [x1,x2] = [x,x] by TARSKI:def 1;
then A3: ( x1 = x & x2 = x ) by XTUPLE_0:1;
reconsider x11 = x1, x22 = x2 as Element of XX by A1, A2, XTUPLE_0:1;
( ff . x11 in U & ff . x22 in U & ff . x11 = ff . x22 ) by A3;
hence [(f . x1),(f . x2)] in R by EQREL_1:5; :: thesis: verum

end;

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