let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds A |^ (n + 1) = (A |^ n) ^^ A
let A be Subset of (E ^omega); :: thesis: for n being Nat holds A |^ (n + 1) = (A |^ n) ^^ A
let n be Nat; :: thesis: A |^ (n + 1) = (A |^ n) ^^ A
consider concat being sequence of (bool (E ^omega)) such that
A1: A |^ n = concat . n and
A2: concat . 0 = {(<%> E)} and
A3: for i being Nat holds concat . (i + 1) = (concat . i) ^^ A by Def2;
concat . (n + 1) = (A |^ n) ^^ A by A1, A3;
hence A |^ (n + 1) = (A |^ n) ^^ A by A2, A3, Def2; :: thesis: verum