let G be Group; :: thesis: for a being Element of G
for A being Subset of G holds
( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )
let a be Element of G; :: thesis: for A being Subset of G holds
( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )
let A be Subset of G; :: thesis: ( (A |^ a) |^ (a ") = A & (A |^ (a ")) |^ a = A )
thus (A |^ a) |^ (a ") = A |^ (a * (a ")) by Th47
.= A |^ (1_ G) by GROUP_1:def 5
.= A by Th52 ; :: thesis: (A |^ (a ")) |^ a = A
thus (A |^ (a ")) |^ a = A |^ ((a ") * a) by Th47
.= A |^ (1_ G) by GROUP_1:def 5
.= A by Th52 ; :: thesis: verum