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