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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (H * a) * b or x in (H * a) * (H * b) )
assume x in (H * a) * b ; :: thesis: x in (H * a) * (H * b)
then x in H * (a * b) by Th40;
then consider g being Element of G such that
A1: x = g * (a * b) and
A2: g in H by Th126;
1_ G in H by Th55;
then A3: ( (1_ G) * b in H * b & g * a in H * a ) by A2, Th126;
x = (g * a) * b by A1, GROUP_1:def 4
.= (g * a) * ((1_ G) * b) by GROUP_1:def 5 ;
hence x in (H * a) * (H * b) by A3; :: thesis: verum