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 and
A3: n <> 0 ; :: thesis: contradiction
<%> E in A * by FLANG_1:48;
hence contradiction by A1, A2, A3, Th10; :: thesis: verum

end;

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

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

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 A4, FLANG_1:36;
hence x in A |^.. n by A5, Th2; :: thesis: verum

end;

end;

end;

then A6: A * c= A |^.. n by TARSKI:def 3;
A |^.. n c= A * by Th9;
hence A |^.. n = A * by A6, XBOOLE_0:def 10; :: thesis: verum