let G be Group; :: thesis: for N being strict normal Subgroup of G
for phi being Automorphism of G holds Image (phi | N) is normal Subgroup of G
let N be strict normal Subgroup of G; :: thesis: for phi being Automorphism of G holds Image (phi | N) is normal Subgroup of G
let phi be Automorphism of G; :: thesis: Image (phi | N) is normal Subgroup of G
set H = Image (phi | N);
for g being Element of G holds g * (Image (phi | N)) = (Image (phi | N)) * g

proof

let g be Element of G; :: thesis: g * (Image (phi | N)) = (Image (phi | N)) * g
set f = (phi ") . g;
B1: phi . ((phi ") . g) = g by Th4;
B2: phi .: (((phi ") . g) * N) = (phi . ((phi ") . g)) * (phi .: N) by Th47
.= g * (Image (phi | N)) by B1, GRSOLV_1:def 3 ;
phi .: (N * ((phi ") . g)) = (phi .: N) * (phi . ((phi ") . g)) by Th48
.= (phi .: N) * g by Th4
.= (Image (phi | N)) * g by GRSOLV_1:def 3 ;
hence g * (Image (phi | N)) = (Image (phi | N)) * g by B2, GROUP_3:117; :: thesis: verum

end;

hence Image (phi | N) is normal Subgroup of G by GROUP_3:117; :: thesis: verum