:: deftheorem defines involutive PARTIT_2:def 2 :
for f being Function holds
( f is involutive iff for x being set st x in dom f holds
f . (f . x) = x );