let L be non empty 1-sorted ; :: thesis: for f being Function of L,L st f is idempotent holds
for x being Element of L holds f . (f . x) = f . x
let p be Function of L,L; :: thesis: ( p is idempotent implies for x being Element of L holds p . (p . x) = p . x )
assume A1: p * p = p ; :: according to QUANTAL1:def 9 :: thesis: for x being Element of L holds p . (p . x) = p . x
let l be Element of L; :: thesis: p . (p . l) = p . l
thus p . (p . l) = p . l by A1, FUNCT_2:15; :: thesis: verum