let A be non empty set ; :: thesis: for f being UnOp of A st f is idempotent holds
for a being Element of A holds f . (f . a) = f . a
let f be UnOp of A; :: thesis: ( f is idempotent implies for a being Element of A holds f . (f . a) = f . a )
assume f * f = f ; :: according to QUANTAL1:def 9 :: thesis: for a being Element of A holds f . (f . a) = f . a
hence for a being Element of A holds f . (f . a) = f . a by FUNCT_2:21; :: thesis: verum