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 S1[ 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 S2[ Nat] means A |^ $1 <> {} ;
assume A4: A <> {} ; :: thesis: contradiction
A5: now :: thesis: for n being Nat st S2[n] holds
S2[n + 1]
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume S2[n] ; :: thesis: S2[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 S2[n + 1] by Th23; :: thesis: verum
end;
A |^ 0 = {(<%> E)} by Th24;
then A8: S2[ 0 ] ;
for n being Nat holds S2[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 & S1[m] holds
S1[m + 1]
let m be Nat; :: thesis: ( 1 <= m & S1[m] implies S1[m + 1] )
assume that
1 <= m and
S1[m] ; :: thesis: S1[m + 1]
({} (E ^omega)) |^ (m + 1) = (({} (E ^omega)) |^ m) ^^ ({} (E ^omega)) by Th23
.= {} by Th12 ;
hence S1[m + 1] by A10; :: thesis: verum
end;
A12: S1[1] by A10, Th25;
A13: for m being Nat st m >= 1 holds
S1[m] from NAT_1:sch 8(A12, A11);
 n >= 0 + 1 by A9, NAT_1:13;
hence A |^ n = {} by A13; :: thesis: verum