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 Th33;
hence A |^ g c= ((g ") * A) * g by GROUP_2:3; :: according to XBOOLE_0:def 10 :: thesis: ((g ") * A) * g c= A |^ g
let x be object ; :: 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:28;
consider b being Element of G such that
A3: a = (g ") * b and
A4: b in A by A2, GROUP_2:27;
x = b |^ g by A1, A3;
hence x in A |^ g by A4, Th41; :: thesis: verum