let G be Group; :: thesis: 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 )
let H be Subgroup of G; :: thesis: 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 )
let a, b be Element of G; :: thesis: ( a * H = b * H implies ex h being Element of G st
( a = b * h & h in H ) )
a in a * H by GROUP_2:108;
hence ( a * H = b * H implies ex h being Element of G st
( a = b * h & h in H ) ) by GROUP_2:103; :: thesis: verum