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;