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 Th77;
A1: ( g (*) (g ") = id X & (g ") (*) g = id X ) by FUNCT_2:61;
reconsider b = g " as Element of (GPerms X) by Th77;
reconsider b = b as Element of (GPerms X) ;
A2: b [*] f = g (*) (g ") by Th70;
( id X = 1_ (GPerms X) & f [*] b = (g ") (*) g ) by Th70, Th78;
hence f " = f " by A1, A2, GROUP_1:def 5; :: thesis: verum