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

for H, K being strict Subgroup of G holds

( z in (H * x) * K iff ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) )

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

( z in (H * x) * K iff ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) )

let H, K be strict Subgroup of G; :: thesis: ( z in (H * x) * K iff ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) )

thus ( z in (H * x) * K implies ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) ) :: thesis: ( ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) implies z in (H * x) * K )

A5: g in H and

A6: h in K ; :: thesis: z in (H * x) * K

ex g1, g2 being Element of G st

( z = g1 * g2 & g1 in H * x & g2 in K ) by A5, A4, A6, GROUP_2:104;

hence z in (H * x) * K by GROUP_2:94; :: thesis: verum

for H, K being strict Subgroup of G holds

( z in (H * x) * K iff ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) )

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

( z in (H * x) * K iff ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) )

let H, K be strict Subgroup of G; :: thesis: ( z in (H * x) * K iff ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) )

thus ( z in (H * x) * K implies ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) ) :: thesis: ( ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) implies z in (H * x) * K )

proof

given g, h being Element of G such that A4:
z = (g * x) * h
and
assume
z in (H * x) * K
; :: thesis: ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K )

then consider g1, g2 being Element of G such that

A1: z = g1 * g2 and

A2: g1 in H * x and

A3: g2 in K by GROUP_2:94;

ex h1 being Element of G st

( g1 = h1 * x & h1 in H ) by A2, GROUP_2:104;

hence ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) by A1, A3; :: thesis: verum

end;( z = (g * x) * h & g in H & h in K )

then consider g1, g2 being Element of G such that

A1: z = g1 * g2 and

A2: g1 in H * x and

A3: g2 in K by GROUP_2:94;

ex h1 being Element of G st

( g1 = h1 * x & h1 in H ) by A2, GROUP_2:104;

hence ex g, h being Element of G st

( z = (g * x) * h & g in H & h in K ) by A1, A3; :: thesis: verum

A5: g in H and

A6: h in K ; :: thesis: z in (H * x) * K

ex g1, g2 being Element of G st

( z = g1 * g2 & g1 in H * x & g2 in K ) by A5, A4, A6, GROUP_2:104;

hence z in (H * x) * K by GROUP_2:94; :: thesis: verum