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 & g1 in H * x & g2 in K ) by GROUP_2:114;
consider h1 being Element of G such that
A2: ( g1 = h1 * x & h1 in H ) by A1, GROUP_2:126;
thus ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) by A1, A2; :: thesis: verum

end;

given g, h being Element of G such that A3: ( z = (g * x) * h & g in H & 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 A3, GROUP_2:126;
hence ex g1, g2 being Element of G st
( z = g1 * g2 & g1 in H * x & g2 in K ) by A3; :: thesis: verum

end;

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