let L be non empty 1-sorted ; :: thesis: for p being Function of L,L st p is idempotent holds
for x being set st x in rng p holds
p . x = x
let p be Function of L,L; :: thesis: ( p is idempotent implies for x being set st x in rng p holds
p . x = x )
assume A1: p is idempotent ; :: thesis: for x being set st x in rng p holds
p . x = x
let x be set ; :: thesis: ( x in rng p implies p . x = x )
assume x in rng p ; :: thesis: p . x = x
then ex a being object st
( a in dom p & x = p . a ) by FUNCT_1:def 3;
hence p . x = x by A1, YELLOW_2:18; :: thesis: verum