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

proof

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

per cases ( ( not <%> E in A & n <> 1 ) or ( n <= 1 & n <> 1 ) ) by A2;

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

per cases ( n = 0 or n > 1 ) by A3, NAT_1:25;

suppose n = 0 ; :: thesis: contradiction

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

end;

suppose A4: n > 1 ; :: thesis: contradiction

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 ( ( a = <%> E & b = <%x%> ) or ( b = <%> E & a = <%x%> ) ) by A8, FLANG_1:4;

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

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

end;

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

hence contradiction by A3, A7; :: thesis: verum

end;

end;

end;

end;

end;

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

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

end;

end;

end;

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

per cases ( ( <%> E in A & n > 1 ) or n = 1 ) by A11;

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

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

end;

suppose n = 1 ; :: thesis: <%x%> in A |^ n

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

end;

end;