let E, x be set ; :: thesis:
let A be Subset of (E ^omega); :: thesis:
let n be Nat; :: thesis:
thus ( <%x%> in A |^ n implies ( <%x%> in A & ( ( <%> E in A & n > 1 ) or n = 1 ) ) ) :: thesis:

proof

assume A1: <%x%> in A |^ n ; :: thesis:
A |^ n c= A * by FLANG_1:42;
hence <%x%> in A by A1, FLANG_1:72; :: thesis:
assume A2: ( ( not <%> E in A or n <= 1 ) & n <> 1 ) ; :: thesis:

per cases by A2;

suppose A3: ( not <%> E in A & n <> 1 ) ; :: thesis:

per cases by A3, NAT_1:25;

suppose n = 0 ; :: thesis:

then A |^ n = {(<%> E)} by FLANG_1:24;
hence contradiction by A1, TARSKI:def 1; :: thesis:

end;

suppose A4: n > 1 ; :: thesis:

then consider m being Nat such that
A5: m + 1 = n by NAT_1:6;
<%x%> in (A |^ m) ^^ A by A1, A5, FLANG_1:23;
then consider a, b being Element of E ^omega such that
A6: a in A |^ m and
A7: b in A and
A8: <%x%> = a ^ b by FLANG_1:def 1;

per cases by A8, FLANG_1:4;

suppose A9: ( a = <%> E & b = <%x%> ) ; :: thesis:

m + 1 > 0 + 1 by A4, A5;
then m > 0 ;
hence contradiction by A3, A6, A9, FLANG_1:31; :: thesis:

end;

suppose ( b = <%> E & a = <%x%> ) ; :: thesis:

hence contradiction by A3, A7; :: thesis:

end;

end;

end;

end;

end;

suppose ( n <= 1 & n <> 1 ) ; :: thesis:

then n = 0 by NAT_1:25;
then A |^ n = {(<%> E)} by FLANG_1:24;
hence contradiction by A1, TARSKI:def 1; :: thesis:

end;

end;

end;

assume that
A10: <%x%> in A and
A11: ( ( <%> E in A & n > 1 ) or n = 1 ) ; :: thesis:

per cases by A11;

suppose ( <%> E in A & n > 1 ) ; :: thesis:

then A c= A |^ n by FLANG_1:35;
hence <%x%> in A |^ n by A10; :: thesis:

end;

suppose n = 1 ; :: thesis:

hence <%x%> in A |^ n by A10, FLANG_1:25; :: thesis:

end;

end;