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