theorem Th16: :: GROUP_22:16

for G being Group
for H being Subgroup of G
for phi being Automorphism of G st ( for f being Automorphism of G holds Image (f | H) is Subgroup of H ) holds
ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) is Subgroup of Image (phi | H) )