let x be set ; :: thesis: for G being Group
for H being strict Subgroup of G holds
( x in Normalizator H iff ex h being Element of G st
( x = h & H |^ h = H ) )
let G be Group; :: thesis: for H being strict Subgroup of G holds
( x in Normalizator H iff ex h being Element of G st
( x = h & H |^ h = H ) )
let H be strict Subgroup of G; :: thesis: ( x in Normalizator H iff ex h being Element of G st
( x = h & H |^ h = H ) )
thus ( x in Normalizator 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 Normalizator H )

proof

assume x in Normalizator 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 Th154;
H |^ a = H by A2, Def6;
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 Normalizator H
(carr H) |^ h = carr H by A4, Def6;
hence x in Normalizator H by A3, Th154; :: thesis: verum