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:35, FLANG_1:61;
(A |^ n) * c= A * by FLANG_1:64;
hence (A |^ n) * = A * by A1, XBOOLE_0:def 10; :: thesis: verum