let E be set ; :: thesis: for A being Subset of (E ^omega)

for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1))

let A be Subset of (E ^omega); :: thesis: for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1))

let n be Nat; :: thesis: A * = (A |^ (0,n)) \/ (A |^.. (n + 1))

thus A * = A |^.. 0 by Th11

.= (A |^ (0,n)) \/ (A |^.. (n + 1)) by Th7 ; :: thesis: verum

for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1))

let A be Subset of (E ^omega); :: thesis: for n being Nat holds A * = (A |^ (0,n)) \/ (A |^.. (n + 1))

let n be Nat; :: thesis: A * = (A |^ (0,n)) \/ (A |^.. (n + 1))

thus A * = A |^.. 0 by Th11

.= (A |^ (0,n)) \/ (A |^.. (n + 1)) by Th7 ; :: thesis: verum