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 ;

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

hence
f is {[x,x]},R -respecting
; :: thesis: verum[(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;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