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