let G be Group; :: thesis: for N being strict normal Subgroup of G
for K being characteristic Subgroup of N holds K is normal Subgroup of G
let N be strict normal Subgroup of G; :: thesis: for K being characteristic Subgroup of N holds K is normal Subgroup of G
let K be characteristic Subgroup of N; :: thesis: K is normal Subgroup of G
for a being Element of G holds K |^ a = multMagma(# the carrier of K, the multF of K #)

proof

let a be Element of G; :: thesis: K |^ a = multMagma(# the carrier of K, the multF of K #)
consider g being inner Automorphism of G such that
A1: a is_inner_wrt g by Th32;
Image (g | N) = N by Th33;
then reconsider f = g | N as Automorphism of N by Th22;
A2: 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;
then ( Image (g | K) = multMagma(# the carrier of K, the multF of K #) & Image (g | K) = K |^ a ) by A1, A2, Th28, Th36;
hence K |^ a = multMagma(# the carrier of K, the multF of K #) ; :: thesis: verum

end;

hence K is normal Subgroup of G by GROUP_3:def 13; :: thesis: verum