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 )

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

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

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