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