let G be Group; :: thesis: for a being Element of G
for H being strict Subgroup of G holds
( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )
let a be Element of G; :: thesis: for H being strict Subgroup of G holds
( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )
let H be strict Subgroup of G; :: thesis: ( (H |^ a) |^ (a ") = H & (H |^ (a ")) |^ a = H )
thus (H |^ a) |^ (a ") = H |^ (a * (a ")) by Th60
.= H |^ (1_ G) by GROUP_1:def 5
.= H by Th61 ; :: thesis: (H |^ (a ")) |^ a = H
thus (H |^ (a ")) |^ a = H |^ ((a ") * a) by Th60
.= H |^ (1_ G) by GROUP_1:def 5
.= H by Th61 ; :: thesis: verum