set h = f " ;
(f ") " = f by FUNCT_1:43;
then ((f ") * (f ")) " = f * f by FUNCT_1:44
.= id A by Th9
.= (id A) " by FUNCT_1:45 ;
hence f " is involutive by Th4, Th10; :: thesis: verum