let x be set ; :: thesis: for G being addGroup
for H being strict Subgroup of G holds
( x in Normalizer H iff ex h being Element of G st
( x = h & H * h = H ) )
let G be addGroup; :: thesis: for H being strict Subgroup of G holds
( x in Normalizer H iff ex h being Element of G st
( x = h & H * h = H ) )
let H be strict Subgroup of G; :: thesis: ( x in Normalizer H iff ex h being Element of G st
( x = h & H * h = H ) )
thus ( x in Normalizer H implies ex h being Element of G st
( x = h & H * h = H ) ) :: thesis: ( ex h being Element of G st
( x = h & H * h = H ) implies x in Normalizer H )

proof

assume x in Normalizer H ; :: thesis: ex h being Element of G st
( x = h & H * h = H )
then consider a being Element of G such that
A1: x = a and
A2: (carr H) * a = carr H by Th129;
H * a = H by A2, Def6A;
hence ex h being Element of G st
( x = h & H * h = H ) by A1; :: thesis: verum

end;

given h being Element of G such that A3: x = h and
A4: H * h = H ; :: thesis: x in Normalizer H
(carr H) * h = carr H by A4, Def6A;
hence x in Normalizer H by A3, Th129; :: thesis: verum