let E be set ; :: thesis: for A being Subset of (E ^omega )
for n being Nat holds (A |^ 1,n) ? = A |^ 0 ,n
let A be Subset of (E ^omega ); :: thesis: for n being Nat holds (A |^ 1,n) ? = A |^ 0 ,n
let n be Nat; :: thesis: (A |^ 1,n) ? = A |^ 0 ,n
thus (A |^ 1,n) ? = {(<%> E)} \/ (A |^ 1,n) by Th76
.= (A |^ 0 ,0 ) \/ (A |^ (0 + 1),n) by Th45
.= A |^ 0 ,n by Th25 ; :: thesis: verum