:: deftheorem defines idempotent QUANTAL1:def 9 :
for f being Function holds
( f is idempotent iff f * f = f );