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 )

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

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 A2:
(b ") * a in H
; :: thesis: a * H = b * H
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;((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

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