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 ) by FLANG_1:48, Th10; :: thesis: ( ( <%> E in A or n = 0 ) implies A |^.. n = A * )
assume A1: ( <%> E in A or n = 0 ) ; :: thesis: A |^.. n = A *

now :: thesis: for x being object st x in A * holds
x in A |^.. n

let x be object ; :: 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
A2: 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 A2, Th2; :: thesis: verum

end;

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

then A |^ k c= A |^ n by A1, FLANG_1:36;
hence x in A |^.. n by A2, Th2; :: thesis: verum

end;

end;

end;

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