let G be strict Group; 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; 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; ( 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 ) )
( ex g, h being Element of G st
( z = (g * x) * h & g in H & h in K ) implies z in (H * x) * K )
given g, h being Element of G such that A4:
z = (g * x) * h
and
A5:
g in H
and
A6:
h in K
; 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; verum