let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )
let A be Subset of (E ^omega); :: thesis: for n being Nat holds
( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )
let n be Nat; :: thesis: ( A |^.. n = {(<%> E)} iff ( A = {(<%> E)} or ( n = 0 & A = {} ) ) )
thus ( not A |^.. n = {(<%> E)} or A = {(<%> E)} or ( n = 0 & A = {} ) ) :: thesis: ( ( A = {(<%> E)} or ( n = 0 & A = {} ) ) implies A |^.. n = {(<%> E)} )

proof

assume that
A1: A |^.. n = {(<%> E)} and
A2: A <> {(<%> E)} and
A3: ( n <> 0 or A <> {} ) ; :: thesis: contradiction

per cases ( n <> 0 or A <> {} ) by A3;

suppose A4: n <> 0 ; :: thesis: contradiction

<%> E in A |^.. n by A1, ZFMISC_1:31;
then consider k being Nat such that
A5: n <= k and
A6: <%> E in A |^ k by Th2;
k > 0 by A4, A5;
then A7: <%> E in A by A6, FLANG_1:31;
for x being object holds
( not x in A or not x <> <%> E ) by A1, Th14;
hence contradiction by A2, A7, ZFMISC_1:35; :: thesis: verum

end;

suppose A <> {} ; :: thesis: contradiction

then ex x being object st
( x in A & x <> <%> E ) by A2, ZFMISC_1:35;
hence contradiction by A1, Th14; :: thesis: verum

end;

end;

end;

assume A8: ( A = {(<%> E)} or ( n = 0 & A = {} ) ) ; :: thesis: A |^.. n = {(<%> E)}

per cases ( A = {(<%> E)} or ( n = 0 & A = {} ) ) by A8;

suppose A9: A = {(<%> E)} ; :: thesis: A |^.. n = {(<%> E)}

A10: now :: thesis: for x being object st x in {(<%> E)} holds
x in A |^.. n

let x be object ; :: thesis: ( x in {(<%> E)} implies x in A |^.. n )
assume x in {(<%> E)} ; :: thesis: x in A |^.. n
then x in A |^ n by A9, FLANG_1:28;
hence x in A |^.. n by Th2; :: thesis: verum

end;

now :: thesis: for x being object st x in A |^.. n holds
x in {(<%> E)}

let x be object ; :: thesis: ( x in A |^.. n implies x in {(<%> E)} )
assume x in A |^.. n ; :: thesis: x in {(<%> E)}
then ex k being Nat st
( n <= k & x in A |^ k ) by Th2;
hence x in {(<%> E)} by A9, FLANG_1:28; :: thesis: verum

end;

hence A |^.. n = {(<%> E)} by A10, TARSKI:2; :: thesis: verum

end;

suppose A11: ( n = 0 & A = {} ) ; :: thesis: A |^.. n = {(<%> E)}

hence A |^.. n = A * by Th11
.= {(<%> E)} by A11, FLANG_1:47 ;
:: thesis: verum

end;

end;