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

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