let A be set ; :: thesis: for f being involutive Function of A,A holds f * f = id A
let f be involutive Function of A,A; :: thesis: f * f = id A
A1: dom f = A by FUNCT_2:52;
then rng f c= dom f ;
hence f * f = id A by A1, Th7; :: thesis: verum