let U be non empty set ; :: thesis: for X, x being 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 X, x be 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 B0: 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

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 CC1: [x1,x2] = [x,x] by TARSKI:def 1;
then C1: ( x1 = x & x2 = x ) by ZFMISC_1:27;
reconsider x11 = x1, x22 = x2 as Element of XX by B0, CC1, ZFMISC_1:27;
( ff . x11 in U & ff . x22 in U & ff . x11 = ff . x22 ) by C1;
hence [(f . x1),(f . x2)] in R by EQREL_1:5; :: thesis: verum

end;

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