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

proof

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

per cases ( m > n or ( m <= n & A <> {(<%> E)} & ( m <> 0 or ( n <> 0 & A <> {} ) ) ) ) by A2;

suppose m > n ; :: thesis: contradiction

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

end;

suppose A3: ( m <= n & A <> {(<%> E)} & ( m <> 0 or ( n <> 0 & A <> {} ) ) ) ; :: thesis: contradiction

per cases ( m <> 0 or ( n <> 0 & A <> {} ) ) by A3;

suppose A4: m <> 0 ; :: thesis: contradiction

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: contradiction

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

end;

suppose A <> {} ; :: thesis: contradiction

then ex x being set st
( x in A & x <> <%> E ) by A3, ZFMISC_1:41;
hence contradiction by A1, A4, Th30; :: thesis: verum

end;

end;

end;

suppose A5: ( n <> 0 & A <> {} ) ; :: thesis: contradiction

then ex x being set st
( x in A & x <> <%> E ) by A3, ZFMISC_1:41;
hence contradiction by A1, A5, Th30; :: thesis: verum

end;

end;

end;

end;

end;

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

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

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

A8: now

let x be set ; :: thesis: ( x in {(<%> E)} implies x in A |^ m,n )
assume x in {(<%> E)} ; :: thesis: x in A |^ m,n
then A9: x in {(<%> E)} |^ m by FLANG_1:30;
{(<%> E)} |^ m c= {(<%> E)} |^ m,n by A7, Th20;
hence x in A |^ m,n by A7, A9; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in A |^ m,n implies x in {(<%> E)} )
assume x in A |^ m,n ; :: thesis: x in {(<%> E)}
then ex k being Nat st
( m <= k & k <= n & x in {(<%> E)} |^ k ) by A7, Th19;
hence x in {(<%> E)} by FLANG_1:30; :: thesis: verum

end;

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

end;

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

A |^ 0 ,0 = A |^ 0 by Th22
.= {(<%> E)} by FLANG_1:30 ;
hence A |^ m,n = {(<%> E)} by A10; :: thesis: verum

end;

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

now

let x be set ; :: thesis: not x in A |^ 1,n
assume x in A |^ 1,n ; :: thesis: contradiction
then ex k being Nat st
( 1 <= k & k <= n & x in A |^ k ) by Th19;
hence contradiction by A11, FLANG_1:28; :: thesis: verum

end;

then A12: A |^ 1,n = {} by XBOOLE_0:def 1;
A |^ 0 ,n = (A |^ 0 ,0 ) \/ (A |^ (0 + 1),n) by Th25
.= (A |^ 0 ) \/ (A |^ (0 + 1),n) by Th22
.= {(<%> E)} by A12, FLANG_1:30 ;
hence A |^ m,n = {(<%> E)} by A11; :: thesis: verum

end;

end;