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 & K ./. ((K,H) `*`) is characteristic Subgroup of G ./. H holds
K is characteristic Subgroup of G
let H be strict characteristic Subgroup of G; :: thesis: for K being strict Subgroup of G st H is Subgroup of K & K ./. ((K,H) `*`) is characteristic Subgroup of G ./. H holds
K is characteristic Subgroup of G
let K be strict Subgroup of G; :: thesis: ( H is Subgroup of K & K ./. ((K,H) `*`) is characteristic Subgroup of G ./. H implies K is characteristic Subgroup of G )
assume A1: H is Subgroup of K ; :: thesis: ( not K ./. ((K,H) `*`) is characteristic Subgroup of G ./. H or K is characteristic Subgroup of G )
assume A2: K ./. ((K,H) `*`) is characteristic Subgroup of G ./. H ; :: thesis: K is characteristic Subgroup of G
A3: (K,H) `*` = H by A1, GROUP_6:def 1;
for phi being Automorphism of G
for k being Element of G st k in K holds
phi . k in K

proof

let phi be Automorphism of G; :: thesis: for k being Element of G st k in K holds
phi . k in K
let k be Element of G; :: thesis: ( k in K implies phi . k in K )
assume B1: k in K ; :: thesis: phi . k in K
Image (phi | H) = H by Def3;
then consider sigma being Automorphism of (G ./. H) such that
B2: for x being Element of G holds sigma . (x * H) = (phi . x) * H by Th73;
consider J being strict characteristic Subgroup of G ./. H such that
B3: J = K ./. ((K,H) `*`) by A2;
B4: for k1 being Element of G st k1 * H in J holds
k1 in K

proof

let k1 be Element of G; :: thesis: ( k1 * H in J implies k1 in K )
assume C1: k1 * H in J ; :: thesis: k1 in K
C2: k1 * H = k1 * ((K,H) `*`) by A1, GROUP_6:def 1;
set x = k1 * ((K,H) `*`);
consider a being Element of K such that
C3: k1 * ((K,H) `*`) = a * ((K,H) `*`) by B3, C1, C2, GROUP_2:def 15;
reconsider a1 = a as Element of G by GROUP_2:42;
C4: a1 in K ;
for j1 being object holds
( j1 in a * ((K,H) `*`) iff j1 in a1 * H )

proof

let j1 be object ; :: thesis: ( j1 in a * ((K,H) `*`) iff j1 in a1 * H )
thus ( j1 in a * ((K,H) `*`) implies j1 in a1 * H ) :: thesis: ( j1 in a1 * H implies j1 in a * ((K,H) `*`) )

proof

assume j1 in a * ((K,H) `*`) ; :: thesis: j1 in a1 * H
then consider g1 being Element of K such that
D1: ( j1 = a * g1 & g1 in (K,H) `*` ) by GROUP_2:103;
reconsider g = g1 as Element of G by GROUP_2:42;
D2: j1 = a1 * g by D1, GROUP_2:43;
g in H by D1, A1, GROUP_6:def 1;
hence j1 in a1 * H by D2, GROUP_2:103; :: thesis: verum

end;

assume j1 in a1 * H ; :: thesis: j1 in a * ((K,H) `*`)
then consider g1 being Element of G such that
D1: ( j1 = a1 * g1 & g1 in H ) by GROUP_2:103;
reconsider g = g1 as Element of K by A1, D1, GROUP_2:42;
D2: j1 = a * g by D1, GROUP_2:43;
g in (K,H) `*` by D1, A1, GROUP_6:def 1;
hence j1 in a * ((K,H) `*`) by D2, GROUP_2:103; :: thesis: verum

end;

then a1 * H = k1 * ((K,H) `*`) by TARSKI:2, C3
.= k1 * H by A1, GROUP_6:def 1 ;
then (a1 ") * k1 in H by GROUP_2:114;
then C5: (a1 ") * k1 in K by A1, GROUP_2:41;
a1 * ((a1 ") * k1) = (a1 * (a1 ")) * k1 by GROUP_1:def 3
.= (1_ G) * k1 by GROUP_1:def 5
.= k1 by GROUP_1:def 4 ;
hence k1 in K by C4, C5, GROUP_2:50; :: thesis: verum

end;

B5: for k1 being Element of G holds
( k1 in K iff k1 * H in J )

proof

let k1 be Element of G; :: thesis: ( k1 in K iff k1 * H in J )
thus ( k1 in K implies k1 * H in J ) :: thesis: ( k1 * H in J implies k1 in K )

proof

assume k1 in K ; :: thesis: k1 * H in J
then reconsider k2 = k1 as Element of K ;
C1: k2 * ((K,H) `*`) in J by B3, GROUP_2:def 15;
for x being object holds
( x in k2 * (carr ((K,H) `*`)) iff x in k1 * (carr H) )

proof

let x be object ; :: thesis: ( x in k2 * (carr ((K,H) `*`)) iff x in k1 * (carr H) )
thus ( x in k2 * (carr ((K,H) `*`)) implies x in k1 * (carr H) ) :: thesis: ( x in k1 * (carr H) implies x in k2 * (carr ((K,H) `*`)) )

proof

assume E1: x in k2 * (carr ((K,H) `*`)) ; :: thesis: x in k1 * (carr H)
( x in k2 * ((K,H) `*`) iff ex g being Element of K st
( x = k2 * g & g in (K,H) `*` ) ) by GROUP_2:103;
then consider huh being Element of K such that
E2: ( x = k2 * huh & huh in (K,H) `*` ) by E1;
E3: huh in H by A1, E2, GROUP_6:def 1;
reconsider huh2 = huh as Element of G by GROUP_2:42;
set x2 = k1 * huh2;
x = k1 * huh2 by E2, GROUP_2:43;
hence x in k1 * (carr H) by E3, GROUP_2:27; :: thesis: verum

end;

assume x in k1 * (carr H) ; :: thesis: x in k2 * (carr ((K,H) `*`))
then consider h1 being Element of G such that
D1: ( x = k1 * h1 & h1 in carr H ) by GROUP_2:27;
reconsider h2 = h1 as Element of K by A1, D1, GROUP_2:42;
reconsider H1 = H as normal Subgroup of K by A3;
D2: the carrier of H = the carrier of ((K,H) `*`) by A1, GROUP_6:def 1;
k2 * h2 in k2 * (carr H1) by D1, GROUP_2:27;
hence x in k2 * (carr ((K,H) `*`)) by D1, D2, GROUP_2:43; :: thesis: verum

end;

then k2 * (carr ((K,H) `*`)) = k1 * (carr H) by TARSKI:2
.= k1 * H ;
hence k1 * H in J by C1; :: thesis: verum

end;

thus ( k1 * H in J implies k1 in K ) by B4; :: thesis: verum

end;

then k * H in J by B1;
then reconsider kH = k * H as Element of (G ./. H) by GROUP_2:42;
sigma . kH in J by Th50, B1, B5;
then ( sigma . (k * H) in J & sigma . (k * H) = (phi . k) * H ) by B2;
hence phi . k in K by B4; :: thesis: verum

end;

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