let E be set ; :: thesis: for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k c= A *
let A be Subset of (E ^omega); :: thesis: for k being Nat holds (A ?) |^ k c= A *
let k be Nat; :: thesis: (A ?) |^ k c= A *
(A ?) |^ k = (A |^ (0,1)) |^ k by Th79;
hence (A ?) |^ k c= A * by Th32, FLANG_1:59; :: thesis: verum