theorem Th73: :: GROUP_22:68
for G being Group
for N being strict normal Subgroup of G
for phi being Automorphism of G st Image (phi | N) = N holds
ex sigma being Automorphism of (G ./. N) st
for x being Element of G holds sigma . (x * N) = (phi . x) * N