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 } )
set M = { 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 }
A2: rng f c= { x where x is Element of S : x = f . x }

proof

let y be object ; :: 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 reconsider y9 = y as Element of S ;
ex x being object st
( x in dom f & y = f . x ) by A3, FUNCT_1:def 3;
then y9 = f . y9 by A1, FUNCT_1:13;
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 object ; :: 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 A4: ex y9 being Element of S st
( y9 = y & y9 = f . y9 ) ;
dom f = the carrier of S by FUNCT_2:def 1;
hence y in rng f by A4, FUNCT_1:def 3; :: thesis: verum

end;

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