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 b1 in A |^.. n )
assume x in A * ; :: thesis: b1 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: b1 in A |^.. n
hence x in A |^.. n by A2, Th2; :: thesis: verum
end;
suppose k < n ; :: thesis: b1 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