let G be Group; :: thesis: for a being Element of G

for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")

let a be Element of G; :: thesis: for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")

let H2 be Subgroup of G; :: thesis: ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")

set A = (a * H2) * (a ");

set x = the Element of a * H2;

A1: a * H2 <> {} by Th108;

then reconsider x = the Element of a * H2 as Element of G by Lm1;

hence ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") by A8, A2, Th52; :: thesis: verum

for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")

let a be Element of G; :: thesis: for H2 being Subgroup of G ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")

let H2 be Subgroup of G; :: thesis: ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ")

set A = (a * H2) * (a ");

set x = the Element of a * H2;

A1: a * H2 <> {} by Th108;

then reconsider x = the Element of a * H2 as Element of G by Lm1;

A2: now :: thesis: for g being Element of G st g in (a * H2) * (a ") holds

g " in (a * H2) * (a ")

g " in (a * H2) * (a ")

let g be Element of G; :: thesis: ( g in (a * H2) * (a ") implies g " in (a * H2) * (a ") )

assume g in (a * H2) * (a ") ; :: thesis: g " in (a * H2) * (a ")

then consider g1 being Element of G such that

A3: g = g1 * (a ") and

A4: g1 in a * H2 by Th28;

consider g2 being Element of G such that

A5: g1 = a * g2 and

A6: g2 in H2 by A4, Th103;

g2 " in H2 by A6, Th51;

then A7: (g2 ") * (a ") in H2 * (a ") by Th104;

g " = ((a ") ") * ((a * g2) ") by A3, A5, GROUP_1:17

.= a * ((g2 ") * (a ")) by GROUP_1:17 ;

then g " in a * (H2 * (a ")) by A7, Th27;

hence g " in (a * H2) * (a ") by Th10; :: thesis: verum

end;assume g in (a * H2) * (a ") ; :: thesis: g " in (a * H2) * (a ")

then consider g1 being Element of G such that

A3: g = g1 * (a ") and

A4: g1 in a * H2 by Th28;

consider g2 being Element of G such that

A5: g1 = a * g2 and

A6: g2 in H2 by A4, Th103;

g2 " in H2 by A6, Th51;

then A7: (g2 ") * (a ") in H2 * (a ") by Th104;

g " = ((a ") ") * ((a * g2) ") by A3, A5, GROUP_1:17

.= a * ((g2 ") * (a ")) by GROUP_1:17 ;

then g " in a * (H2 * (a ")) by A7, Th27;

hence g " in (a * H2) * (a ") by Th10; :: thesis: verum

A8: now :: thesis: for g1, g2 being Element of G st g1 in (a * H2) * (a ") & g2 in (a * H2) * (a ") holds

g1 * g2 in (a * H2) * (a ")

x * (a ") in (a * H2) * (a ")
by A1, Th28;g1 * g2 in (a * H2) * (a ")

let g1, g2 be Element of G; :: thesis: ( g1 in (a * H2) * (a ") & g2 in (a * H2) * (a ") implies g1 * g2 in (a * H2) * (a ") )

assume that

A9: g1 in (a * H2) * (a ") and

A10: g2 in (a * H2) * (a ") ; :: thesis: g1 * g2 in (a * H2) * (a ")

consider g being Element of G such that

A11: g1 = g * (a ") and

A12: g in a * H2 by A9, Th28;

consider h being Element of G such that

A13: g = a * h and

A14: h in H2 by A12, Th103;

(a * H2) * (a ") = a * (H2 * (a ")) by Th10;

then consider b being Element of G such that

A15: g2 = a * b and

A16: b in H2 * (a ") by A10, Th27;

consider c being Element of G such that

A17: b = c * (a ") and

A18: c in H2 by A16, Th104;

h * c in H2 by A14, A18, Th50;

then A19: a * (h * c) in a * H2 by Th103;

g1 * g2 = (a * h) * ((a ") * (a * (c * (a ")))) by A11, A15, A13, A17, GROUP_1:def 3

.= (a * h) * (((a ") * a) * (c * (a "))) by GROUP_1:def 3

.= (a * h) * ((1_ G) * (c * (a "))) by GROUP_1:def 5

.= (a * h) * (c * (a ")) by GROUP_1:def 4

.= ((a * h) * c) * (a ") by GROUP_1:def 3

.= (a * (h * c)) * (a ") by GROUP_1:def 3 ;

hence g1 * g2 in (a * H2) * (a ") by A19, Th28; :: thesis: verum

end;assume that

A9: g1 in (a * H2) * (a ") and

A10: g2 in (a * H2) * (a ") ; :: thesis: g1 * g2 in (a * H2) * (a ")

consider g being Element of G such that

A11: g1 = g * (a ") and

A12: g in a * H2 by A9, Th28;

consider h being Element of G such that

A13: g = a * h and

A14: h in H2 by A12, Th103;

(a * H2) * (a ") = a * (H2 * (a ")) by Th10;

then consider b being Element of G such that

A15: g2 = a * b and

A16: b in H2 * (a ") by A10, Th27;

consider c being Element of G such that

A17: b = c * (a ") and

A18: c in H2 by A16, Th104;

h * c in H2 by A14, A18, Th50;

then A19: a * (h * c) in a * H2 by Th103;

g1 * g2 = (a * h) * ((a ") * (a * (c * (a ")))) by A11, A15, A13, A17, GROUP_1:def 3

.= (a * h) * (((a ") * a) * (c * (a "))) by GROUP_1:def 3

.= (a * h) * ((1_ G) * (c * (a "))) by GROUP_1:def 5

.= (a * h) * (c * (a ")) by GROUP_1:def 4

.= ((a * h) * c) * (a ") by GROUP_1:def 3

.= (a * (h * c)) * (a ") by GROUP_1:def 3 ;

hence g1 * g2 in (a * H2) * (a ") by A19, Th28; :: thesis: verum

hence ex H1 being strict Subgroup of G st the carrier of H1 = (a * H2) * (a ") by A8, A2, Th52; :: thesis: verum