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

proof

assume that
A1: A |^.. n = A * and
A2: ( not <%> E in A & n <> 0 ) ; :: thesis: contradiction
( <%> E in A * & not <%> E in A |^.. n ) by A2, Th10, FLANG_1:49;
hence contradiction by A1; :: thesis: verum

end;

assume A3: ( <%> E in A or n = 0 ) ; :: thesis: A |^.. n = A *

per cases ( <%> E in A or n = 0 ) by A3;

suppose <%> E in A ; :: thesis: A |^.. n = A *

A4: A |^.. n c= A * by Th9;
A * c= A |^.. n

proof

now

let x be set ; :: thesis: ( x in A * implies b₁ in A |^.. n )
assume x in A * ; :: thesis: b₁ in A |^.. n
then consider k being Nat such that
A5: x in A |^ k by FLANG_1:42;

per cases ( n <= k or k < n ) ;

suppose n <= k ; :: thesis: b₁ in A |^.. n

hence x in A |^.. n by A5, Th2; :: thesis: verum

end;

suppose k < n ; :: thesis: b₁ in A |^.. n

then A |^ k c= A |^ n by A3, FLANG_1:37;
hence x in A |^.. n by A5, Th2; :: thesis: verum

end;

end;

end;

hence A * c= A |^.. n by TARSKI:def 3; :: thesis: verum

end;

hence A |^.. n = A * by A4, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A6: n = 0 ; :: thesis: A |^.. n = A *

A7: now

let x be set ; :: thesis: ( x in A |^.. n implies x in A * )
assume x in A |^.. n ; :: thesis: x in A *
then consider k being Nat such that
A8: ( 0 <= k & x in A |^ k ) by A6, Th2;
thus x in A * by A8, FLANG_1:42; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in A * implies x in A |^.. n )
assume x in A * ; :: thesis: x in A |^.. n
then consider k being Nat such that
A9: x in A |^ k by FLANG_1:42;
thus x in A |^.. n by A6, A9, Th2; :: thesis: verum

end;

hence A |^.. n = A * by A7, TARSKI:2; :: thesis: verum

end;

end;