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, Th67;
hence ( (f " ) * f = id X & f * (f " ) = id X ) by FUNCT_1:61; :: thesis: verum