let X be set ; :: thesis: for x being Element of (SymGroup X) holds x " = x "
let x be Element of (SymGroup X); :: thesis: x " = x "
reconsider f = x as Permutation of X by Th5;
f " in permutations X ;
then reconsider g = f " as Element of (SymGroup X) by Def2;
A1: 1_ (SymGroup X) = id X by Th6;
x * g = g * x by Def2;
then A2: x * g = id X by FUNCT_2:61;
g * x = x * g by Def2;
then g * x = id X by FUNCT_2:61;
hence x " = x " by A2, A1, GROUP_1:def 5; :: thesis: verum