theorem Th17: :: GROUP_22:17

for G being Group
for H being Subgroup of G
for phi being Automorphism of G ex psi being Automorphism of G st
( psi = phi " & Image (phi | (Image (psi | H))) = multMagma(# the carrier of H, the multF of H #) )