theorem :: FOMODEL0:72

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