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 Th72
.= H |^ (1_ G) by GROUP_1:def 6
.= H by Th73 ; :: thesis: (H |^ (a " )) |^ a = H
thus (H |^ (a " )) |^ a = H |^ ((a " ) * a) by Th72
.= H |^ (1_ G) by GROUP_1:def 6
.= H by Th73 ; :: thesis: verum