let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds A + = (A |^ (1,n)) \/ (A |^.. (n + 1))
let A be Subset of (E ^omega); :: thesis: for n being Nat holds A + = (A |^ (1,n)) \/ (A |^.. (n + 1))
let n be Nat; :: thesis: A + = (A |^ (1,n)) \/ (A |^.. (n + 1))
A1: 0 + 1 <= n + 1 by XREAL_1:7;
thus A + = A |^.. 1 by Th50
.= (A |^ (1,n)) \/ (A |^.. (n + 1)) by A1, Th7 ; :: thesis: verum