let E be set ; :: thesis: for A, B being Subset of (E ^omega)
for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
let A, B be Subset of (E ^omega); :: thesis: for n being Nat holds (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
let n be Nat; :: thesis: (A /\ B) |^ n c= (A |^ n) /\ (B |^ n)
( (A /\ B) |^ n c= A |^ n & (A /\ B) |^ n c= B |^ n ) by Th37, XBOOLE_1:17;
hence (A /\ B) |^ n c= (A |^ n) /\ (B |^ n) by XBOOLE_1:19; :: thesis: verum