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