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

proof

assume A1: a * H = b * H ; :: thesis: (b " ) * a in H
((b " ) * a) * H = (b " ) * (a * H) by Th38
.= ((b " ) * b) * H by A1, Th38
.= (1_ G) * H by GROUP_1:def 6
.= carr H by Th43 ;
hence (b " ) * a in H by Th136; :: thesis: verum

end;

assume A2: (b " ) * a in H ; :: thesis: a * H = b * H
thus a * H = (1_ G) * (a * H) by Th43
.= ((1_ G) * a) * H by Th38
.= ((b * (b " )) * a) * H by GROUP_1:def 6
.= (b * ((b " ) * a)) * H by GROUP_1:def 4
.= b * (((b " ) * a) * H) by Th38
.= b * H by A2, Th136 ; :: thesis: verum