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 object ; :: 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 and
A2: a in A by Th42;
a " in A " by A2;
then (a ") * g in (A ") * g by GROUP_2:28;
hence x in ((A ") * g) * A by A1, A2; :: thesis: verum