let S be non empty 1-sorted ; :: thesis: for f being Function of S,S st f is idempotent holds
rng f = { x where x is Element of S : x = f . x }
let f be Function of S,S; :: thesis: ( f is idempotent implies rng f = { x where x is Element of S : x = f . x } )
assume A1: f = f * f ; :: according to QUANTAL1:def 9 :: thesis: rng f = { x where x is Element of S : x = f . x }
set M = { x where x is Element of S : x = f . x } ;
A2: rng f c= { x where x is Element of S : x = f . x }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { x where x is Element of S : x = f . x } )
assume A3: y in rng f ; :: thesis: y in { x where x is Element of S : x = f . x }
then consider x being set such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def 5;
reconsider y' = y as Element of S by A3;
y' = f . y' by A1, A4, A5, FUNCT_1:23;
hence y in { x where x is Element of S : x = f . x } ; :: thesis: verum

end;

{ x where x is Element of S : x = f . x } c= rng f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of S : x = f . x } or y in rng f )
assume y in { x where x is Element of S : x = f . x } ; :: thesis: y in rng f
then consider y' being Element of S such that
A6: y' = y and
A7: y' = f . y' ;
dom f = the carrier of S by FUNCT_2:def 1;
hence y in rng f by A6, A7, FUNCT_1:def 5; :: thesis: verum

end;

hence rng f = { x where x is Element of S : x = f . x } by A2, XBOOLE_0:def 10; :: thesis: verum