let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A & n > 0 holds
A c= A |^ n
let A be Subset of (E ^omega); :: thesis: for n being Nat st <%> E in A & n > 0 holds
A c= A |^ n
let n be Nat; :: thesis: ( <%> E in A & n > 0 implies A c= A |^ n )
assume that
A1: <%> E in A and
A2: n > 0 ; :: thesis: A c= A |^ n
consider m being Nat such that
A3: m + 1 = n by A2, NAT_1:6;
<%> E in A |^ m by A1, Th30;
then A c= (A |^ m) ^^ A by Th16;
hence A c= A |^ n by A3, Th23; :: thesis: verum