let x, E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat st m <> n & A |^ m = {x} & A |^ n = {x} holds
x = <%> E
let A be Subset of (E ^omega ); :: thesis: for m, n being Nat st m <> n & A |^ m = {x} & A |^ n = {x} holds
x = <%> E
let m, n be Nat; :: thesis: ( m <> n & A |^ m = {x} & A |^ n = {x} implies x = <%> E )
assume A1: ( m <> n & A |^ m = {x} & A |^ n = {x} ) ; :: thesis: x = <%> E
then A2: ( x in A |^ m & x in A |^ n ) by TARSKI:def 1;

per cases ( m > n or m < n ) by A1, XXREAL_0:1;

suppose m > n ; :: thesis: x = <%> E

then consider k being Nat such that
A3: ( n + k = m & k > 0 ) by Th3;
(A |^ n) ^^ (A |^ k) = A |^ m by A3, FLANG_1:34;
then consider a, b being Element of E ^omega such that
A4: ( a in A |^ n & b in A |^ k & x = a ^ b ) by A2, FLANG_1:def 1;
a = x by A1, A4, TARSKI:def 1;
then b = <%> E by A4, Th4;
then <%> E in A by A3, A4, FLANG_1:32;
then ( <%> E in A |^ m & <%> E in A |^ n ) by FLANG_1:31;
hence x = <%> E by A1, TARSKI:def 1; :: thesis: verum

end;

suppose m < n ; :: thesis: x = <%> E

then consider k being Nat such that
A5: ( m + k = n & k > 0 ) by Th3;
(A |^ m) ^^ (A |^ k) = A |^ n by A5, FLANG_1:34;
then consider a, b being Element of E ^omega such that
A6: ( a in A |^ m & b in A |^ k & x = a ^ b ) by A2, FLANG_1:def 1;
a = x by A1, A6, TARSKI:def 1;
then b = <%> E by A6, Th4;
then <%> E in A by A5, A6, FLANG_1:32;
then ( <%> E in A |^ m & <%> E in A |^ n ) by FLANG_1:31;
hence x = <%> E by A1, TARSKI:def 1; :: thesis: verum

end;

end;