let G be Group; :: thesis: for g being Element of G
for A being Subset of G holds A |^ g = ((g " ) * A) * g
let g be Element of G; :: thesis: for A being Subset of G holds A |^ g = ((g " ) * A) * g
let A be Subset of G; :: thesis: A |^ g = ((g " ) * A) * g
A |^ g c= (({g} " ) * A) * {g} by Th40;
hence A |^ g c= ((g " ) * A) * g by GROUP_2:6; :: according to XBOOLE_0:def 10 :: thesis: ((g " ) * A) * g c= A |^ g
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in ((g " ) * A) * g or x in A |^ g )
assume x in ((g " ) * A) * g ; :: thesis: x in A |^ g
then consider a being Element of G such that
A1: x = a * g and
A2: a in (g " ) * A by GROUP_2:34;
consider b being Element of G such that
A3: a = (g " ) * b and
A4: b in A by A2, GROUP_2:33;
x = b |^ g by A1, A3;
hence x in A |^ g by A4, Th50; :: thesis: verum