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

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