let G be Group; :: thesis: for a, b being Element of G
for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H)
let a, b be Element of G; :: thesis: for H being Subgroup of G holds (a * b) * H c= (a * H) * (b * H)
let H be Subgroup of G; :: thesis: (a * b) * H c= (a * H) * (b * H)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (a * b) * H or x in (a * H) * (b * H) )
assume x in (a * b) * H ; :: thesis: x in (a * H) * (b * H)
then consider g being Element of G such that
A1: x = (a * b) * g and
A2: g in H by Th103;
A3: x = ((a * (1_ G)) * b) * g by A1, GROUP_1:def 4
.= (a * (1_ G)) * (b * g) by GROUP_1:def 3 ;
1_ G in H by Th46;
then A4: a * (1_ G) in a * H by Th103;
b * g in b * H by A2, Th103;
hence x in (a * H) * (b * H) by A3, A4; :: thesis: verum