let E be set ; :: thesis: for A being Subset of (E ^omega)
for k being Nat holds (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))
let A be Subset of (E ^omega); :: thesis: for k being Nat holds (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))
let k be Nat; :: thesis: (A ?) ^^ (A |^ k) = A |^ (k,(k + 1))
(A |^ (0,1)) ^^ (A |^ k) = (A |^ (0,1)) ^^ (A |^ (k,k)) by Th22
.= A |^ ((0 + k),(1 + k)) by Th37 ;
hence (A ?) ^^ (A |^ k) = A |^ (k,(k + 1)) by Th79; :: thesis: verum