let E, x 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 and
A2: x <> <%> E and
A3: ( 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 A3;
suppose m > n ; :: thesis: A |^ (m,n) <> {(<%> E)}
hence A |^ (m,n) <> {(<%> E)} by Th21; :: thesis: verum
end;
suppose A4: ( m <= n & m > 0 ) ; :: thesis: A |^ (m,n) <> {(<%> E)}
A5: A |^ m <> {} by A1, FLANG_1:27;
A |^ m <> {(<%> E)} by A1, A2, A4, Th7;
then A6: ex x being object st
( x in A |^ m & x <> <%> E ) by A5, ZFMISC_1:35;
A |^ m c= A |^ (m,n) by A4, Th20;
hence A |^ (m,n) <> {(<%> E)} by A6, TARSKI:def 1; :: thesis: verum
end;
suppose A7: ( m <= n & n > 0 ) ; :: thesis: A |^ (m,n) <> {(<%> E)}
A8: A |^ n <> {} by A1, FLANG_1:27;
A |^ n <> {(<%> E)} by A1, A2, A7, Th7;
then A9: ex x being object st
( x in A |^ n & x <> <%> E ) by A8, ZFMISC_1:35;
A |^ n c= A |^ (m,n) by A7, Th20;
hence A |^ (m,n) <> {(<%> E)} by A9, TARSKI:def 1; :: thesis: verum
end;
end;