let G be finite Group; :: thesis: for H being strict characteristic Subgroup of G
for K being strict Subgroup of G st H is Subgroup of K holds
H is normal Subgroup of K
let H be strict characteristic Subgroup of G; :: thesis: for K being strict Subgroup of G st H is Subgroup of K holds
H is normal Subgroup of K
let K be strict Subgroup of G; :: thesis: ( H is Subgroup of K implies H is normal Subgroup of K )
assume A1: H is Subgroup of K ; :: thesis: H is normal Subgroup of K
A2: for g being Element of G holds
( g in Ker (nat_hom H) iff g in H ) by GROUP_6:43;
reconsider R = Ker ((nat_hom H) | K) as strict Subgroup of K ;
A3: for k being Element of K holds
( k in H iff k in Ker ((nat_hom H) | K) )

proof

let k be Element of K; :: thesis: ( k in H iff k in Ker ((nat_hom H) | K) )
reconsider g = k as Element of G by GROUP_2:42;
B1: g in K ;
thus ( k in H implies k in Ker ((nat_hom H) | K) ) :: thesis: ( k in Ker ((nat_hom H) | K) implies k in H )

proof

assume C1: k in H ; :: thesis: k in Ker ((nat_hom H) | K)
C2: g in K ;
(nat_hom H) . g = 1_ (G ./. H) by A2, C1, GROUP_6:41;
then ((nat_hom H) | K) . g = 1_ (G ./. H) by C2, Th1;
hence k in Ker ((nat_hom H) | K) by GROUP_6:41; :: thesis: verum

end;

thus ( k in Ker ((nat_hom H) | K) implies k in H ) :: thesis: verum

proof

assume C1: k in Ker ((nat_hom H) | K) ; :: thesis: k in H
((nat_hom H) | K) . g = (nat_hom H) . g by B1, Th1;
then (nat_hom H) . g = 1_ (G ./. H) by C1, GROUP_6:41;
then g in Ker (nat_hom H) by GROUP_6:41;
hence k in H by GROUP_6:43; :: thesis: verum

end;

end;

reconsider H1 = H as strict Subgroup of K by A1;
multMagma(# the carrier of R, the multF of R #) = multMagma(# the carrier of H1, the multF of H1 #) by A3, GROUP_2:60;
hence H is normal Subgroup of K ; :: thesis: verum