let R be non empty RelStr ; :: thesis: for f being Function of the carrier of R,(bool the carrier of R) st f is map-reflexive holds

(ff_0 f) . the carrier of R = the carrier of R

let f be Function of the carrier of R,(bool the carrier of R); :: thesis: ( f is map-reflexive implies (ff_0 f) . the carrier of R = the carrier of R )

assume RR: f is map-reflexive ; :: thesis: (ff_0 f) . the carrier of R = the carrier of R

A0: (ff_0 f) . ([#] R) = { u where u is Element of R : f . u meets [#] R } by Defff;

the carrier of R c= { u where u is Element of R : f . u meets [#] R }

(ff_0 f) . the carrier of R = the carrier of R

let f be Function of the carrier of R,(bool the carrier of R); :: thesis: ( f is map-reflexive implies (ff_0 f) . the carrier of R = the carrier of R )

assume RR: f is map-reflexive ; :: thesis: (ff_0 f) . the carrier of R = the carrier of R

A0: (ff_0 f) . ([#] R) = { u where u is Element of R : f . u meets [#] R } by Defff;

the carrier of R c= { u where u is Element of R : f . u meets [#] R }

proof

hence
(ff_0 f) . the carrier of R = the carrier of R
by A0; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in the carrier of R or y in { u where u is Element of R : f . u meets [#] R } )

assume y in the carrier of R ; :: thesis: y in { u where u is Element of R : f . u meets [#] R }

then reconsider u = y as Element of R ;

u in f . u by RR;

then consider u being Element of R such that

A1: ( u = y & f . u meets [#] R ) by XBOOLE_0:3;

thus y in { u where u is Element of R : f . u meets [#] R } by A1; :: thesis: verum

end;assume y in the carrier of R ; :: thesis: y in { u where u is Element of R : f . u meets [#] R }

then reconsider u = y as Element of R ;

u in f . u by RR;

then consider u being Element of R such that

A1: ( u = y & f . u meets [#] R ) by XBOOLE_0:3;

thus y in { u where u is Element of R : f . u meets [#] R } by A1; :: thesis: verum