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 consider a being set such that
A2: a in dom p and
A3: x = p . a by FUNCT_1:def 5;
thus p . x = x by A1, A2, A3, YELLOW_2:20; :: thesis: verum