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