let G be Group; :: thesis: for g being Element of G
for A being Subset of G holds g |^ A c= ((A " ) * g) * A
let g be Element of G; :: thesis: for A being Subset of G holds g |^ A c= ((A " ) * g) * A
let A be Subset of G; :: thesis: g |^ A c= ((A " ) * g) * A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in g |^ A or x in ((A " ) * g) * A )
assume x in g |^ A ; :: thesis: x in ((A " ) * g) * A
then consider a being Element of G such that
A1: ( x = g |^ a & a in A ) by Th51;
a " in A " by A1;
then (a " ) * g in (A " ) * g by GROUP_2:34;
hence x in ((A " ) * g) * A by A1; :: thesis: verum