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