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 Th32
.= ((b ") * b) * H by A1, Th32
.= (1_ G) * H by GROUP_1:def 5
.= carr H by Th37 ;
hence (b ") * a in H by Th113; :: thesis: verum

end;

assume A2: (b ") * a in H ; :: thesis: a * H = b * H
thus a * H = (1_ G) * (a * H) by Th37
.= ((1_ G) * a) * H by Th32
.= ((b * (b ")) * a) * H by GROUP_1:def 5
.= (b * ((b ") * a)) * H by GROUP_1:def 3
.= b * (((b ") * a) * H) by Th32
.= b * H by A2, Th113 ; :: thesis: verum