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

(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