let X be set ; :: thesis: for f being Permutation of X holds
( (f ") * f = id X & f * (f ") = id X )
let f be Permutation of X; :: thesis: ( (f ") * f = id X & f * (f ") = id X )
( dom f = X & rng f = X ) by Def3, Th51;
hence ( (f ") * f = id X & f * (f ") = id X ) by FUNCT_1:39; :: thesis: verum