let G be Group; :: thesis: for a, b being Element of G
for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b)
let a, b be Element of G; :: thesis: for A being Subset of G holds (A |^ a) |^ b = A |^ (a * b)
let A be Subset of G; :: thesis: (A |^ a) |^ b = A |^ (a * b)
thus (A |^ a) |^ b = A |^ (a * {b}) by Th35
.= A |^ (a * b) by GROUP_2:18 ; :: thesis: verum