theorem Th9: :: GROUPP_1:9

for G being Group
for H being Subgroup of G
for a, b being Element of G st a * H = b * H holds
ex h being Element of G st
( a = b * h & h in H ) by GROUP_2:108, GROUP_2:103;