let G be Group; :: thesis: for a, b being Element of G
for H being Subgroup of G holds
( H * a = H * b iff b * (a ") in H )
let a, b be Element of G; :: thesis: for H being Subgroup of G holds
( H * a = H * b iff b * (a ") in H )
let H be Subgroup of G; :: thesis: ( H * a = H * b iff b * (a ") in H )
thus ( H * a = H * b implies b * (a ") in H ) :: thesis: ( b * (a ") in H implies H * a = H * b )

proof

assume A1: H * a = H * b ; :: thesis: b * (a ") in H
carr H = H * (1_ G) by Th37
.= H * (a * (a ")) by GROUP_1:def 5
.= (H * b) * (a ") by A1, Th34
.= H * (b * (a ")) by Th34 ;
hence b * (a ") in H by Th119; :: thesis: verum

end;

assume b * (a ") in H ; :: thesis: H * a = H * b
hence H * a = (H * (b * (a "))) * a by Th119
.= H * ((b * (a ")) * a) by Th34
.= H * (b * ((a ") * a)) by GROUP_1:def 3
.= H * (b * (1_ G)) by GROUP_1:def 5
.= H * b by GROUP_1:def 4 ;
:: thesis: verum