let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat holds
( A |^ n = {} iff ( n > 0 & A = {} ) )
let A be Subset of (E ^omega); :: thesis: for n being Nat holds
( A |^ n = {} iff ( n > 0 & A = {} ) )
let n be Nat; :: thesis: ( A |^ n = {} iff ( n > 0 & A = {} ) )
defpred S₁[ Nat] means A |^ $1 = {} ;
thus ( A |^ n = {} implies ( n > 0 & A = {} ) ) :: thesis: ( n > 0 & A = {} implies A |^ n = {} )

proof

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

A3: now :: thesis: not A <> {}

defpred S₂[ Nat] means A |^ $1 <> {} ;
assume A4: A <> {} ; :: thesis: contradiction

A5: now :: thesis: for n being Nat st S₂[n] holds
S₂[n + 1]

let n be Nat; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume S₂[n] ; :: thesis: S₂[n + 1]
then consider a1 being Element of E ^omega such that
A6: a1 in A |^ n by SUBSET_1:4;
consider a2 being Element of E ^omega such that
A7: a2 in A by A4, SUBSET_1:4;
a1 ^ a2 in (A |^ n) ^^ A by A6, A7, Def1;
hence S₂[n + 1] by Th23; :: thesis: verum

end;

A |^ 0 = {(<%> E)} by Th24;
then A8: S₂[ 0 ] ;
for n being Nat holds S₂[n] from NAT_1:sch 2(A8, A5);
hence contradiction by A1; :: thesis: verum

end;

now :: thesis: not n <= 0

assume n <= 0 ; :: thesis: contradiction
then n = 0 ;
then A |^ n = {(<%> E)} by Th24;
hence contradiction by A1; :: thesis: verum

end;

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

end;

assume that
A9: n > 0 and
A10: A = {} ; :: thesis: A |^ n = {}

A11: now :: thesis: for m being Nat st 1 <= m & S₁[m] holds
S₁[m + 1]

let m be Nat; :: thesis: ( 1 <= m & S₁[m] implies S₁[m + 1] )
assume that
1 <= m and
S₁[m] ; :: thesis: S₁[m + 1]
({} (E ^omega)) |^ (m + 1) = (({} (E ^omega)) |^ m) ^^ ({} (E ^omega)) by Th23
.= {} by Th12 ;
hence S₁[m + 1] by A10; :: thesis: verum

end;

A12: S₁[1] by A10, Th25;
A13: for m being Nat st m >= 1 holds
S₁[m] from NAT_1:sch 8(A12, A11);
n >= 0 + 1 by A9, NAT_1:13;
hence A |^ n = {} by A13; :: thesis: verum