let E be set ; :: thesis: for A being Subset of
for n being Nat holds A |^ (n + 1) = (A |^ n) ^^ A
let A be Subset of ; :: 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 Function of NAT , 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