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)} )

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 A8:
( A = {(<%> E)} or ( n = 0 & A = {} ) )
; :: thesis: A |^.. n = {(<%> E)}
assume that

A1: A |^.. n = {(<%> E)} and

A2: A <> {(<%> E)} and

A3: ( n <> 0 or A <> {} ) ; :: thesis: contradiction

end;A1: A |^.. n = {(<%> E)} and

A2: A <> {(<%> E)} and

A3: ( n <> 0 or A <> {} ) ; :: thesis: contradiction

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

end;

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;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

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;( x in A & x <> <%> E ) by A2, ZFMISC_1:35;

hence contradiction by A1, Th14; :: thesis: verum

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

end;

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

end;

A10: now :: thesis: for x being object st x in {(<%> E)} holds

x in A |^.. n

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;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

now :: thesis: for x being object st x in A |^.. n holds

x in {(<%> E)}

hence
A |^.. n = {(<%> E)}
by A10, TARSKI:2; :: thesis: verumx 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;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