let G be strict Group; :: thesis: for z, x 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 z, x 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

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:114;
ex h1 being Element of G st
( g1 = h1 * x & h1 in H ) by A2, GROUP_2:126;
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;

given g, h being Element of G such that A4: z = (g * x) * h and
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 )

proof

set g1 = g * x;
g * x in H * x by A5, GROUP_2:126;
hence ex g1, g2 being Element of G st
( z = g1 * g2 & g1 in H * x & g2 in K ) by A4, A6; :: thesis: verum

end;

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