let E, x 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 that
A1: m <> n and
A2: A |^ m = {x} and
A3: A |^ n = {x} ; :: thesis: x = <%> E
A4: x in A |^ m by A2, TARSKI:def 1;
A5: x in A |^ n by A3, 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
A6: n + k = m and
A7: k > 0 by Th3;
(A |^ n) ^^ (A |^ k) = A |^ m by A6, FLANG_1:33;
then consider a, b being Element of E ^omega such that
A8: a in A |^ n and
A9: b in A |^ k and
A10: x = a ^ b by A4, FLANG_1:def 1;
a = x by A3, A8, TARSKI:def 1;
then b = <%> E by A10, Th4;
then <%> E in A by A7, A9, FLANG_1:31;
then <%> E in A |^ m by FLANG_1:30;
hence x = <%> E by A2; :: thesis: verum
end;
suppose m < n ; :: thesis: x = <%> E
then consider k being Nat such that
A11: m + k = n and
A12: k > 0 by Th3;
(A |^ m) ^^ (A |^ k) = A |^ n by A11, FLANG_1:33;
then consider a, b being Element of E ^omega such that
A13: a in A |^ m and
A14: b in A |^ k and
A15: x = a ^ b by A5, FLANG_1:def 1;
a = x by A2, A13, TARSKI:def 1;
then b = <%> E by A15, Th4;
then <%> E in A by A12, A14, FLANG_1:31;
then <%> E in A |^ m by FLANG_1:30;
hence x = <%> E by A2; :: thesis: verum
end;
end;