for f being Function st f is involutive holds
f * f c= id (dom f) by Lm65;