let G be Group; :: thesis: for a, b being Element of G

for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)

let a, b be Element of G; :: thesis: for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)

let H be Subgroup of G; :: thesis: (H * a) * b c= (H * a) * (H * b)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (H * a) * b or x in (H * a) * (H * b) )

1_ G in H by Th46;

then A1: (1_ G) * b in H * b by Th104;

assume x in (H * a) * b ; :: thesis: x in (H * a) * (H * b)

then x in H * (a * b) by Th34;

then consider g being Element of G such that

A2: x = g * (a * b) and

A3: g in H by Th104;

A4: x = (g * a) * b by A2, GROUP_1:def 3

.= (g * a) * ((1_ G) * b) by GROUP_1:def 4 ;

g * a in H * a by A3, Th104;

hence x in (H * a) * (H * b) by A1, A4; :: thesis: verum

for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)

let a, b be Element of G; :: thesis: for H being Subgroup of G holds (H * a) * b c= (H * a) * (H * b)

let H be Subgroup of G; :: thesis: (H * a) * b c= (H * a) * (H * b)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (H * a) * b or x in (H * a) * (H * b) )

1_ G in H by Th46;

then A1: (1_ G) * b in H * b by Th104;

assume x in (H * a) * b ; :: thesis: x in (H * a) * (H * b)

then x in H * (a * b) by Th34;

then consider g being Element of G such that

A2: x = g * (a * b) and

A3: g in H by Th104;

A4: x = (g * a) * b by A2, GROUP_1:def 3

.= (g * a) * ((1_ G) * b) by GROUP_1:def 4 ;

g * a in H * a by A3, Th104;

hence x in (H * a) * (H * b) by A1, A4; :: thesis: verum