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

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