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:9;
thus A + = A |^.. 1 by Th50
.= (A |^ 1,n) \/ (A |^.. (n + 1)) by A1, Th7 ; :: thesis: verum