let G be strict Group; :: thesis: for x, y being Element of G

for H, K being strict Subgroup of G holds

( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

let x, y be Element of G; :: thesis: for H, K being strict Subgroup of G holds

( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

let H, K be strict Subgroup of G; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

for H, K being strict Subgroup of G holds

( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

let x, y be Element of G; :: thesis: for H, K being strict Subgroup of G holds

( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

let H, K be strict Subgroup of G; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

per cases
( for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) or ex z being Element of G st

( z in (H * x) * K & z in (H * y) * K ) ) ;

end;

( not z in (H * x) * K or not z in (H * y) * K ) or ex z being Element of G st

( z in (H * x) * K & z in (H * y) * K ) ) ;

suppose
for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) ; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

( not z in (H * x) * K or not z in (H * y) * K ) ; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

hence
( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) ) ; :: thesis: verum

end;( not z in (H * x) * K or not z in (H * y) * K ) ) ; :: thesis: verum

suppose
ex z being Element of G st

( z in (H * x) * K & z in (H * y) * K ) ; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

( z in (H * x) * K & z in (H * y) * K ) ; :: thesis: ( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) )

then consider z being Element of G such that

A1: z in (H * x) * K and

A2: z in (H * y) * K ;

consider h1, k1 being Element of G such that

A3: z = (h1 * x) * k1 and

A4: h1 in H and

A5: k1 in K by A1, Th17;

consider h2, k2 being Element of G such that

A6: z = (h2 * y) * k2 and

A7: h2 in H and

A8: k2 in K by A2, Th17;

for a being object st a in (H * x) * K holds

a in (H * y) * K

for a being object st a in (H * y) * K holds

a in (H * x) * K

hence ( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) ) by A15, XBOOLE_0:def 10; :: thesis: verum

end;A1: z in (H * x) * K and

A2: z in (H * y) * K ;

consider h1, k1 being Element of G such that

A3: z = (h1 * x) * k1 and

A4: h1 in H and

A5: k1 in K by A1, Th17;

consider h2, k2 being Element of G such that

A6: z = (h2 * y) * k2 and

A7: h2 in H and

A8: k2 in K by A2, Th17;

for a being object st a in (H * x) * K holds

a in (H * y) * K

proof

then A15:
(H * x) * K c= (H * y) * K
;
let a be object ; :: thesis: ( a in (H * x) * K implies a in (H * y) * K )

assume a in (H * x) * K ; :: thesis: a in (H * y) * K

then consider h, k being Element of G such that

A9: a = (h * x) * k and

A10: h in H and

A11: k in K by Th17;

ex c, d being Element of G st

( a = (c * y) * d & c in H & d in K )

end;assume a in (H * x) * K ; :: thesis: a in (H * y) * K

then consider h, k being Element of G such that

A9: a = (h * x) * k and

A10: h in H and

A11: k in K by Th17;

ex c, d being Element of G st

( a = (c * y) * d & c in H & d in K )

proof

hence
a in (H * y) * K
by Th17; :: thesis: verum
h = h * (1_ G)
by GROUP_1:def 4;

then A12: (h * x) * k = (((h * (1_ G)) * x) * (1_ G)) * k by GROUP_1:def 4;

1_ G = (h1 ") * h1 by GROUP_1:def 5;

then A13: (h * x) * k = (((h * ((h1 ") * h1)) * x) * (k1 * (k1 "))) * k by A12, GROUP_1:def 5

.= ((((h * ((h1 ") * h1)) * x) * k1) * (k1 ")) * k by GROUP_1:def 3

.= (((((h * (h1 ")) * h1) * x) * k1) * (k1 ")) * k by GROUP_1:def 3

.= ((((h * (h1 ")) * (h1 * x)) * k1) * (k1 ")) * k by GROUP_1:def 3

.= (((h * (h1 ")) * ((h2 * y) * k2)) * (k1 ")) * k by A3, A6, GROUP_1:def 3

.= ((((h * (h1 ")) * (h2 * y)) * k2) * (k1 ")) * k by GROUP_1:def 3

.= (((((h * (h1 ")) * h2) * y) * k2) * (k1 ")) * k by GROUP_1:def 3

.= ((((h * (h1 ")) * h2) * y) * (k2 * (k1 "))) * k by GROUP_1:def 3

.= (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) by GROUP_1:def 3 ;

take (h * (h1 ")) * h2 ; :: thesis: ex d being Element of G st

( a = (((h * (h1 ")) * h2) * y) * d & (h * (h1 ")) * h2 in H & d in K )

take (k2 * (k1 ")) * k ; :: thesis: ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K )

h1 " in H by A4, GROUP_2:51;

then A14: h * (h1 ") in H by A10, GROUP_2:50;

k1 " in K by A5, GROUP_2:51;

then k2 * (k1 ") in K by A8, GROUP_2:50;

hence ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K ) by A7, A9, A11, A13, A14, GROUP_2:50; :: thesis: verum

end;then A12: (h * x) * k = (((h * (1_ G)) * x) * (1_ G)) * k by GROUP_1:def 4;

1_ G = (h1 ") * h1 by GROUP_1:def 5;

then A13: (h * x) * k = (((h * ((h1 ") * h1)) * x) * (k1 * (k1 "))) * k by A12, GROUP_1:def 5

.= ((((h * ((h1 ") * h1)) * x) * k1) * (k1 ")) * k by GROUP_1:def 3

.= (((((h * (h1 ")) * h1) * x) * k1) * (k1 ")) * k by GROUP_1:def 3

.= ((((h * (h1 ")) * (h1 * x)) * k1) * (k1 ")) * k by GROUP_1:def 3

.= (((h * (h1 ")) * ((h2 * y) * k2)) * (k1 ")) * k by A3, A6, GROUP_1:def 3

.= ((((h * (h1 ")) * (h2 * y)) * k2) * (k1 ")) * k by GROUP_1:def 3

.= (((((h * (h1 ")) * h2) * y) * k2) * (k1 ")) * k by GROUP_1:def 3

.= ((((h * (h1 ")) * h2) * y) * (k2 * (k1 "))) * k by GROUP_1:def 3

.= (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) by GROUP_1:def 3 ;

take (h * (h1 ")) * h2 ; :: thesis: ex d being Element of G st

( a = (((h * (h1 ")) * h2) * y) * d & (h * (h1 ")) * h2 in H & d in K )

take (k2 * (k1 ")) * k ; :: thesis: ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K )

h1 " in H by A4, GROUP_2:51;

then A14: h * (h1 ") in H by A10, GROUP_2:50;

k1 " in K by A5, GROUP_2:51;

then k2 * (k1 ") in K by A8, GROUP_2:50;

hence ( a = (((h * (h1 ")) * h2) * y) * ((k2 * (k1 ")) * k) & (h * (h1 ")) * h2 in H & (k2 * (k1 ")) * k in K ) by A7, A9, A11, A13, A14, GROUP_2:50; :: thesis: verum

for a being object st a in (H * y) * K holds

a in (H * x) * K

proof

then
(H * y) * K c= (H * x) * K
;
let a be object ; :: thesis: ( a in (H * y) * K implies a in (H * x) * K )

assume a in (H * y) * K ; :: thesis: a in (H * x) * K

then consider h, k being Element of G such that

A16: a = (h * y) * k and

A17: h in H and

A18: k in K by Th17;

ex c, d being Element of G st

( a = (c * x) * d & c in H & d in K )

end;assume a in (H * y) * K ; :: thesis: a in (H * x) * K

then consider h, k being Element of G such that

A16: a = (h * y) * k and

A17: h in H and

A18: k in K by Th17;

ex c, d being Element of G st

( a = (c * x) * d & c in H & d in K )

proof

hence
a in (H * x) * K
by Th17; :: thesis: verum
h = h * (1_ G)
by GROUP_1:def 4;

then A19: (h * y) * k = (((h * (1_ G)) * y) * (1_ G)) * k by GROUP_1:def 4;

1_ G = (h2 ") * h2 by GROUP_1:def 5;

then A20: (h * y) * k = (((h * ((h2 ") * h2)) * y) * (k2 * (k2 "))) * k by A19, GROUP_1:def 5

.= ((((h * ((h2 ") * h2)) * y) * k2) * (k2 ")) * k by GROUP_1:def 3

.= (((((h * (h2 ")) * h2) * y) * k2) * (k2 ")) * k by GROUP_1:def 3

.= ((((h * (h2 ")) * (h2 * y)) * k2) * (k2 ")) * k by GROUP_1:def 3

.= (((h * (h2 ")) * ((h1 * x) * k1)) * (k2 ")) * k by A3, A6, GROUP_1:def 3

.= ((((h * (h2 ")) * (h1 * x)) * k1) * (k2 ")) * k by GROUP_1:def 3

.= (((((h * (h2 ")) * h1) * x) * k1) * (k2 ")) * k by GROUP_1:def 3

.= ((((h * (h2 ")) * h1) * x) * (k1 * (k2 "))) * k by GROUP_1:def 3

.= (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) by GROUP_1:def 3 ;

take (h * (h2 ")) * h1 ; :: thesis: ex d being Element of G st

( a = (((h * (h2 ")) * h1) * x) * d & (h * (h2 ")) * h1 in H & d in K )

take (k1 * (k2 ")) * k ; :: thesis: ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K )

h2 " in H by A7, GROUP_2:51;

then A21: h * (h2 ") in H by A17, GROUP_2:50;

k2 " in K by A8, GROUP_2:51;

then k1 * (k2 ") in K by A5, GROUP_2:50;

hence ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K ) by A4, A16, A18, A20, A21, GROUP_2:50; :: thesis: verum

end;then A19: (h * y) * k = (((h * (1_ G)) * y) * (1_ G)) * k by GROUP_1:def 4;

1_ G = (h2 ") * h2 by GROUP_1:def 5;

then A20: (h * y) * k = (((h * ((h2 ") * h2)) * y) * (k2 * (k2 "))) * k by A19, GROUP_1:def 5

.= ((((h * ((h2 ") * h2)) * y) * k2) * (k2 ")) * k by GROUP_1:def 3

.= (((((h * (h2 ")) * h2) * y) * k2) * (k2 ")) * k by GROUP_1:def 3

.= ((((h * (h2 ")) * (h2 * y)) * k2) * (k2 ")) * k by GROUP_1:def 3

.= (((h * (h2 ")) * ((h1 * x) * k1)) * (k2 ")) * k by A3, A6, GROUP_1:def 3

.= ((((h * (h2 ")) * (h1 * x)) * k1) * (k2 ")) * k by GROUP_1:def 3

.= (((((h * (h2 ")) * h1) * x) * k1) * (k2 ")) * k by GROUP_1:def 3

.= ((((h * (h2 ")) * h1) * x) * (k1 * (k2 "))) * k by GROUP_1:def 3

.= (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) by GROUP_1:def 3 ;

take (h * (h2 ")) * h1 ; :: thesis: ex d being Element of G st

( a = (((h * (h2 ")) * h1) * x) * d & (h * (h2 ")) * h1 in H & d in K )

take (k1 * (k2 ")) * k ; :: thesis: ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K )

h2 " in H by A7, GROUP_2:51;

then A21: h * (h2 ") in H by A17, GROUP_2:50;

k2 " in K by A8, GROUP_2:51;

then k1 * (k2 ") in K by A5, GROUP_2:50;

hence ( a = (((h * (h2 ")) * h1) * x) * ((k1 * (k2 ")) * k) & (h * (h2 ")) * h1 in H & (k1 * (k2 ")) * k in K ) by A4, A16, A18, A20, A21, GROUP_2:50; :: thesis: verum

hence ( (H * x) * K = (H * y) * K or for z being Element of G holds

( not z in (H * x) * K or not z in (H * y) * K ) ) by A15, XBOOLE_0:def 10; :: thesis: verum