let x, E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat st x in A & x <> <%> E & ( m > 0 or n > 0 ) holds
A |^ m,n <> {(<%> E)}
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat st x in A & x <> <%> E & ( m > 0 or n > 0 ) holds
A |^ m,n <> {(<%> E)}
let m, n be Nat; :: thesis: ( x in A & x <> <%> E & ( m > 0 or n > 0 ) implies A |^ m,n <> {(<%> E)} )
assume that
A1: ( x in A & x <> <%> E ) and
A2: ( m > 0 or n > 0 ) ; :: thesis: A |^ m,n <> {(<%> E)}

per cases ( m > n or ( m <= n & m > 0 ) or ( m <= n & n > 0 ) ) by A2;

suppose m > n ; :: thesis: A |^ m,n <> {(<%> E)}

hence A |^ m,n <> {(<%> E)} by Th21; :: thesis: verum

end;

suppose A3: ( m <= n & m > 0 ) ; :: thesis: A |^ m,n <> {(<%> E)}

then A4: A |^ m <> {(<%> E)} by A1, Th7;
A |^ m <> {} by A1, FLANG_1:28;
then consider x being set such that
A5: ( x in A |^ m & x <> <%> E ) by A4, ZFMISC_1:41;
A |^ m c= A |^ m,n by A3, Th20;
hence A |^ m,n <> {(<%> E)} by A5, TARSKI:def 1; :: thesis: verum

end;

suppose A6: ( m <= n & n > 0 ) ; :: thesis: A |^ m,n <> {(<%> E)}

then A7: A |^ n <> {(<%> E)} by A1, Th7;
A |^ n <> {} by A1, FLANG_1:28;
then consider x being set such that
A8: ( x in A |^ n & x <> <%> E ) by A7, ZFMISC_1:41;
A |^ n c= A |^ m,n by A6, Th20;
hence A |^ m,n <> {(<%> E)} by A8, TARSKI:def 1; :: thesis: verum

end;

end;