let E be set ; :: thesis: for A being Subset of (E ^omega )
for n being Nat holds (A ? ) |^ 0 ,n = A |^ 0 ,n
let A be Subset of (E ^omega ); :: thesis: for n being Nat holds (A ? ) |^ 0 ,n = A |^ 0 ,n
let n be Nat; :: thesis: (A ? ) |^ 0 ,n = A |^ 0 ,n
thus (A ? ) |^ 0 ,n = (A ? ) |^ n by Th94
.= A |^ 0 ,n by Th95 ; :: thesis: verum