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

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

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

hence x = <%> E by A1, Th21; :: thesis: verum

end;

suppose A2: ( m = 0 & m <= n ) ; :: thesis: x = <%> E

then {(<%> E)} = A |^ m by FLANG_1:25;
then <%> E in A |^ m by TARSKI:def 1;
then <%> E in A |^ m,n by A2, Th19;
hence x = <%> E by A1, TARSKI:def 1; :: thesis: verum

end;

suppose ( m > 0 & m <= n ) ; :: thesis: x = <%> E

then ( A |^ m = {x} & A |^ n = {x} ) by A1, Th51;
hence x = <%> E by A1, Th10; :: thesis: verum

end;

end;