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)
let g be Element of G; :: according to GROUP_2:def 6 :: thesis: ( ( not g in (H1 /\ H2) |^ a or g in (H1 |^ a) /\ (H2 |^ a) ) & ( not g in (H1 |^ a) /\ (H2 |^ a) or g in (H1 /\ H2) |^ a ) )
thus ( g in (H1 /\ H2) |^ a implies g in (H1 |^ a) /\ (H2 |^ a) ) :: thesis: ( not g in (H1 |^ a) /\ (H2 |^ a) or g in (H1 /\ H2) |^ a )

proof

assume g in (H1 /\ H2) |^ a ; :: thesis: g in (H1 |^ a) /\ (H2 |^ a)
then consider h being Element of G such that
A1: ( g = h |^ a & h in H1 /\ H2 ) by Th70;
( h in H1 & h in H2 ) by A1, GROUP_2:99;
then ( g in H1 |^ a & g in H2 |^ a ) by A1, Th70;
hence g in (H1 |^ a) /\ (H2 |^ a) by GROUP_2:99; :: thesis: verum

end;

assume A2: g in (H1 |^ a) /\ (H2 |^ a) ; :: thesis: g in (H1 /\ H2) |^ a
then g in H1 |^ a by GROUP_2:99;
then consider b being Element of G such that
A3: ( g = b |^ a & b in H1 ) by Th70;
g in H2 |^ a by A2, GROUP_2:99;
then consider c being Element of G such that
A4: ( g = c |^ a & c in H2 ) by Th70;
b = c by A3, A4, Th21;
then b in H1 /\ H2 by A3, A4, GROUP_2:99;
hence g in (H1 /\ H2) |^ a by A3, Th70; :: thesis: verum