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

let A be Subset of (); :: 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 ;
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 ;
for x being object holds
( not x in A or not x <> <%> E ) by ;
hence contradiction by A2, A7, ZFMISC_1:35; :: 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 ;
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 ; :: thesis: verum
end;
hence A |^.. n = {(<%> E)} by ; :: thesis: verum
end;
suppose A11: ( n = 0 & A = {} ) ; :: thesis: A |^.. n = {(<%> E)}
hence A |^.. n = A * by Th11
.= {(<%> E)} by ;
:: thesis: verum
end;
end;