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 object ; :: 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 Th104;
g in H2 by ;
then A3: x in H2 * a by ;
g in H1 by ;
then x in H1 * a by ;
hence x in (H1 * a) /\ (H2 * a) by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (H1 * a) /\ (H2 * a) or x in (H1 /\ H2) * a )
assume A4: x in (H1 * a) /\ (H2 * a) ; :: thesis: x in (H1 /\ H2) * a
then x in H1 * a by XBOOLE_0:def 4;
then consider g being Element of G such that
A5: x = g * a and
A6: g in H1 by Th104;
x in H2 * a by ;
then consider g1 being Element of G such that
A7: x = g1 * a and
A8: g1 in H2 by Th104;
g = g1 by ;
then g in H1 /\ H2 by A6, A8, Th82;
hence x in (H1 /\ H2) * a by ; :: thesis: verum