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 Th43
.= H * (a * (a " )) by GROUP_1:def 6
.= (H * b) * (a " ) by A1, Th40
.= H * (b * (a " )) by Th40 ;
hence b * (a " ) in H by Th142; :: thesis: verum

end;

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