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 }

proof

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;

hence (ff_0 f) . the carrier of R = the carrier of R by A0; :: thesis: verum