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

then A2: (A + ) |^ k = {(<%> E)} by FLANG_1:25;
A |^.. 0 = A * by Th11;
then <%> E in A |^.. 0 by FLANG_1:49;
hence (A + ) |^ k c= A |^.. k by A1, A2, ZFMISC_1:37; :: thesis: verum

end;

end;