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

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