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