let G be Group; :: thesis: for K being characteristic Subgroup of G holds K is normal Subgroup of G
let K be characteristic Subgroup of G; :: 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 f being inner Automorphism of G such that
A2: a is_inner_wrt f by Th32;
multMagma(# the carrier of K, the multF of K #) = Image (f | K) by Def3
.= K |^ a by A2, Th28 ;
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