let E, x 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 that
A1: m <> n and
A2: 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 A2, Th21; :: thesis: verum
end;
suppose A3: ( m = 0 & m <= n ) ; :: thesis: x = <%> E
then {(<%> E)} = A |^ m by FLANG_1:24;
then <%> E in A |^ m by TARSKI:def 1;
then <%> E in A |^ (m,n) by A3, Th19;
hence x = <%> E by A2; :: thesis: verum
end;
suppose ( m > 0 & m <= n ) ; :: thesis: x = <%> E
then ( A |^ m = {x} & A |^ n = {x} ) by A2, Th51;
hence x = <%> E by A1, Th10; :: thesis: verum
end;
end;