let E be set ; :: thesis: for A being Subset of (E ^omega)
for k being Nat holds (A +) |^ k c= A |^.. k
let A be Subset of (E ^omega); :: thesis: for k being Nat holds (A +) |^ k c= A |^.. k
let k be Nat; :: thesis: (A +) |^ k c= A |^.. k
per cases ( k > 0 or k = 0 ) ;
suppose k > 0 ; :: thesis: (A +) |^ k c= A |^.. k
then (A |^.. 1) |^ k c= A |^.. (1 * k) by Th19;
hence (A +) |^ k c= A |^.. k by Th50; :: thesis: verum
end;
suppose A1: k = 0 ; :: thesis: (A +) |^ k c= A |^.. k
A |^.. 0 = A * by Th11;
then A2: <%> E in A |^.. 0 by FLANG_1:48;
(A +) |^ k = {(<%> E)} by A1, FLANG_1:24;
hence (A +) |^ k c= A |^.. k by A1, A2, ZFMISC_1:31; :: thesis: verum
end;
end;