let G be Group; :: thesis: for H being Subgroup of G
for h, n being Element of G st h in H & n in Normalizer H holds
h |^ n in H
let H be Subgroup of G; :: thesis: for h, n being Element of G st h in H & n in Normalizer H holds
h |^ n in H
let h, n be Element of G; :: thesis: ( h in H & n in Normalizer H implies h |^ n in H )
assume A1: h in H ; :: thesis: ( not n in Normalizer H or h |^ n in H )
assume n in Normalizer H ; :: thesis: h |^ n in H
then consider g being Element of G such that
A2: ( n " = g & (carr H) |^ g = carr H ) by GROUP_2:51, GROUP_3:129;
consider h1 being Element of G such that
A3: ( h = h1 |^ g & h1 in carr H ) by A1, A2, GROUP_3:41;
h |^ n = (h1 |^ (n ")) |^ n by A2, A3
.= h1 by GROUP_3:25 ;
hence h |^ n in H by A3; :: thesis: verum