let X be set ; :: thesis: for S being non empty 1-sorted
for f being Function of S,S st f is idempotent & X c= rng f holds
f .: X = X
let S be non empty 1-sorted ; :: thesis: for f being Function of S,S st f is idempotent & X c= rng f holds
f .: X = X
let f be Function of S,S; :: thesis: ( f is idempotent & X c= rng f implies f .: X = X )
assume A1: f is idempotent ; :: thesis: ( not X c= rng f or f .: X = X )
set M = { x where x is Element of S : x = f . x } ;
assume X c= rng f ; :: thesis: f .: X = X
then A2: X c= { x where x is Element of S : x = f . x } by A1, Th19;
A3: f .: X c= X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: X or y in X )
assume y in f .: X ; :: thesis: y in X
then consider x being object such that
x in dom f and
A4: x in X and
A5: y = f . x by FUNCT_1:def 6;
x in { x where x is Element of S : x = f . x } by A2, A4;
then ex x9 being Element of S st
( x9 = x & x9 = f . x9 ) ;
hence y in X by A4, A5; :: thesis: verum

end;

X c= f .: X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in f .: X )
assume A6: y in X ; :: thesis: y in f .: X
then y in { x where x is Element of S : x = f . x } by A2;
then ex x being Element of S st
( x = y & x = f . x ) ;
hence y in f .: X by A6, FUNCT_2:35; :: thesis: verum

end;

hence f .: X = X by A3, XBOOLE_0:def 10; :: thesis: verum