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 Th48;
then A1: ( n > 0 implies A * c= (A *) |^ n ) by Th35;
(A *) |^ n c= A * by Th65;
hence ( n > 0 implies (A *) |^ n = A * ) by A1, XBOOLE_0:def 10; :: thesis: verum