let E be set ; :: thesis: for A being Subset of (E ^omega)
for k being Nat holds (A ?) |^ k = (A ?) |^ (0,k)
let A be Subset of (E ^omega); :: thesis: for k being Nat holds (A ?) |^ k = (A ?) |^ (0,k)
let k be Nat; :: thesis: (A ?) |^ k = (A ?) |^ (0,k)
<%> E in A ? by Th78;
hence (A ?) |^ k = (A ?) |^ (0,k) by Th34; :: thesis: verum