let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n being Nat holds
( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )
let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds
( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )
let m, n be Nat; :: thesis: ( A |^ (m,n) = {} iff ( m > n or ( m > 0 & A = {} ) ) )

A1: now :: thesis: ( m > 0 & A = {} implies A |^ (m,n) = {} )

assume A2: ( m > 0 & A = {} ) ; :: thesis: A |^ (m,n) = {}

now :: thesis: for x being object holds not x in A |^ (m,n)

let x be object ; :: thesis: not x in A |^ (m,n)
assume x in A |^ (m,n) ; :: thesis: contradiction
then ex k being Nat st
( m <= k & k <= n & x in A |^ k ) by Th19;
hence contradiction by A2, FLANG_1:27; :: thesis: verum

end;

hence A |^ (m,n) = {} by XBOOLE_0:def 1; :: thesis: verum

end;

thus ( not A |^ (m,n) = {} or m > n or ( m > 0 & A = {} ) ) :: thesis: ( ( m > n or ( m > 0 & A = {} ) ) implies A |^ (m,n) = {} )

proof

assume that
A3: A |^ (m,n) = {} and
A4: ( m <= n & ( m <= 0 or A <> {} ) ) ; :: thesis: contradiction

A5: now :: thesis: ( m <= n implies not A <> {} )

assume that
A6: m <= n and
A7: A <> {} ; :: thesis: contradiction
A |^ m <> {} by A7, FLANG_1:27;
then ex a being Element of E ^omega st a in A |^ m by SUBSET_1:4;
hence contradiction by A3, A6, Th19; :: thesis: verum

end;

now :: thesis: ( m <= n implies not m = 0 )

assume that
A8: m <= n and
A9: m = 0 ; :: thesis: contradiction
{(<%> E)} = A |^ m by A9, FLANG_1:29;
then <%> E in A |^ m by TARSKI:def 1;
hence contradiction by A3, A8, Th19; :: thesis: verum

end;

hence contradiction by A4, A5; :: thesis: verum

end;

now :: thesis: ( m > n implies A |^ (m,n) = {} )

assume A10: m > n ; :: thesis: A |^ (m,n) = {}

now :: thesis: for x being object holds not x in A |^ (m,n)

let x be object ; :: thesis: not x in A |^ (m,n)
for k being Nat holds
( not m <= k or not k <= n or not x in A |^ k ) by A10, XXREAL_0:2;
hence not x in A |^ (m,n) by Th19; :: thesis: verum

end;

hence A |^ (m,n) = {} by XBOOLE_0:def 1; :: thesis: verum

end;

hence ( ( m > n or ( m > 0 & A = {} ) ) implies A |^ (m,n) = {} ) by A1; :: thesis: verum