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