let G be Group; :: thesis: for a being Element of G
for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
let a be Element of G; :: thesis: for H1, H2 being Subgroup of G holds (H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
let H1, H2 be Subgroup of G; :: thesis: (H1 /\ H2) * a = (H1 * a) /\ (H2 * a)
thus (H1 /\ H2) * a c= (H1 * a) /\ (H2 * a) :: according to XBOOLE_0:def 10 :: thesis: (H1 * a) /\ (H2 * a) c= (H1 /\ H2) * a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (H1 /\ H2) * a or x in (H1 * a) /\ (H2 * a) )
assume x in (H1 /\ H2) * a ; :: thesis: x in (H1 * a) /\ (H2 * a)
then consider g being Element of G such that
A1: x = g * a and
A2: g in H1 /\ H2 by Th126;
( g in H1 & g in H2 ) by A2, Th99;
then ( x in H1 * a & x in H2 * a ) by A1, Th126;
hence x in (H1 * a) /\ (H2 * a) by XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (H1 * a) /\ (H2 * a) or x in (H1 /\ H2) * a )
assume x in (H1 * a) /\ (H2 * a) ; :: thesis: x in (H1 /\ H2) * a
then A3: ( x in H1 * a & x in H2 * a ) by XBOOLE_0:def 4;
then consider g being Element of G such that
A4: x = g * a and
A5: g in H1 by Th126;
consider g1 being Element of G such that
A6: x = g1 * a and
A7: g1 in H2 by A3, Th126;
g = g1 by A4, A6, GROUP_1:14;
then g in H1 /\ H2 by A5, A7, Th99;
hence x in (H1 /\ H2) * a by A4, Th126; :: thesis: verum