let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat holds
( <%> E in A |^ m,n iff ( m = 0 or ( m <= n & <%> E in A ) ) )
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat holds
( <%> E in A |^ m,n iff ( m = 0 or ( m <= n & <%> E in A ) ) )
let m, n be Nat; :: thesis: ( <%> E in A |^ m,n iff ( m = 0 or ( m <= n & <%> E in A ) ) )
thus ( not <%> E in A |^ m,n or m = 0 or ( m <= n & <%> E in A ) ) :: thesis: ( ( m = 0 or ( m <= n & <%> E in A ) ) implies <%> E in A |^ m,n )

proof

assume that
A1: <%> E in A |^ m,n and
A2: ( m <> 0 & ( m > n or not <%> E in A ) ) ; :: thesis: contradiction

per cases ( ( m <> 0 & m > n ) or ( m <> 0 & not <%> E in A ) ) by A2;

suppose ( m <> 0 & m > n ) ; :: thesis: contradiction

hence contradiction by A1, Th21; :: thesis: verum

end;

suppose A3: ( m <> 0 & not <%> E in A ) ; :: thesis: contradiction

consider k being Nat such that
A4: m <= k and
k <= n and
A5: <%> E in A |^ k by A1, Th19;
k > 0 by A3, A4;
hence contradiction by A3, A5, FLANG_1:32; :: thesis: verum

end;

end;

end;

assume A6: ( m = 0 or ( m <= n & <%> E in A ) ) ; :: thesis: <%> E in A |^ m,n

per cases ( m = 0 or ( m <= n & <%> E in A ) ) by A6;

suppose A7: m = 0 ; :: thesis: <%> E in A |^ m,n

{(<%> E)} = A |^ 0 by FLANG_1:30;
then A8: {(<%> E)} c= A |^ 0 ,n by Th20;
<%> E in {(<%> E)} by TARSKI:def 1;
hence <%> E in A |^ m,n by A7, A8; :: thesis: verum

end;

suppose ( m <= n & <%> E in A ) ; :: thesis: <%> E in A |^ m,n

then ( <%> E in A |^ m & A |^ m c= A |^ m,n ) by Th20, FLANG_1:31;
hence <%> E in A |^ m,n ; :: thesis: verum

end;

end;