let E be set ; :: thesis: for A being Subset of (E ^omega )
for n being Nat st n > 0 holds
(A * ) |^ n = A *
let A be Subset of (E ^omega ); :: thesis: for n being Nat st n > 0 holds
(A * ) |^ n = A *
let n be Nat; :: thesis: ( n > 0 implies (A * ) |^ n = A * )
<%> E in A * by Th49;
then A1: ( n > 0 implies A * c= (A * ) |^ n ) by Th36;
(A * ) |^ n c= A * by Th66;
hence ( n > 0 implies (A * ) |^ n = A * ) by A1, XBOOLE_0:def 10; :: thesis: verum