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 object st
( x in A & x <> <%> E ) by A3, ZFMISC_1:35;
hence contradiction by A1, A4, Th30; :: thesis: verum

end;

end;

end;

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

then ex x being object st
( x in A & x <> <%> E ) by A3, ZFMISC_1:35;
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 :: thesis: for x being object st x in {(<%> E)} holds
x in A |^ (m,n)

let x be object ; :: 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:29;
{(<%> E)} |^ m c= {(<%> E)} |^ (m,n) by A7, Th20;
hence x in A |^ (m,n) by A7, A9; :: thesis: verum

end;

now :: thesis: for x being object st x in A |^ (m,n) holds
x in {(<%> E)}

let x be object ; :: 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:29; :: 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:29 ;
hence A |^ (m,n) = {(<%> E)} by A10; :: thesis: verum

end;

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

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

let x be object ; :: 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:27; :: 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:29 ;
hence A |^ (m,n) = {(<%> E)} by A11; :: thesis: verum

end;

end;