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 )
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: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;
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 ) by A5, A4, A6, GROUP_2:104;
hence z in (H * x) * K by GROUP_2:94; :: thesis: verum