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;

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

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