let G be Group; :: thesis: for N being characteristic Subgroup of G
for K being characteristic Subgroup of N holds K is characteristic Subgroup of G
let N be characteristic Subgroup of G; :: thesis: for K being characteristic Subgroup of N holds K is characteristic Subgroup of G
let K be characteristic Subgroup of N; :: thesis: K is characteristic Subgroup of G
for g being Automorphism of G holds Image (g | K) = multMagma(# the carrier of K, the multF of K #)

proof

let g be Automorphism of G; :: thesis: Image (g | K) = multMagma(# the carrier of K, the multF of K #)
Image (g | N) = multMagma(# the carrier of N, the multF of N #) by Def3;
then reconsider f = g | N as Automorphism of N by Th22;
A1: Image (f | K) = multMagma(# the carrier of K, the multF of K #) by Def3;
for k being Element of G st k in K holds
f . k = g . k by Th1, GROUP_2:40;
hence Image (g | K) = multMagma(# the carrier of K, the multF of K #) by A1, Th36; :: thesis: verum

end;

hence K is characteristic Subgroup of G by Def3; :: thesis: verum