let X be set ; :: thesis: for f being Element of (GPerms X) holds f " = f "
let f be Element of (GPerms X); :: thesis: f " = f "
reconsider g = f as Permutation of X by Th86;
A1: ( g (*) (g " ) = id X & (g " ) (*) g = id X ) by FUNCT_2:88;
reconsider b = g " as Element of (GPerms X) by Th86;
reconsider b = b as Element of (GPerms X) ;
A2: b [*] f = (g " ) (*) g by Th79;
( id X = 1_ (GPerms X) & f [*] b = g (*) (g " ) ) by Th79, Th87;
hence f " = f " by A1, A2, GROUP_1:def 6; :: thesis: verum