let A be set ; :: thesis: for f being Function of A,A st f * f = id A holds

f is involutive

let f be Function of A,A; :: thesis: ( f * f = id A implies f is involutive )

dom f = A by FUNCT_2:52;

hence ( f * f = id A implies f is involutive ) by Th8; :: thesis: verum

f is involutive

let f be Function of A,A; :: thesis: ( f * f = id A implies f is involutive )

dom f = A by FUNCT_2:52;

hence ( f * f = id A implies f is involutive ) by Th8; :: thesis: verum