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 *

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

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

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

then A3:
A * c= A |^.. n
;x in A |^.. n

let x be object ; :: thesis: ( x in A * implies b_{1} in A |^.. n )

assume x in A * ; :: thesis: b_{1} in A |^.. n

then consider k being Nat such that

A2: x in A |^ k by FLANG_1:41;

end;assume x in A * ; :: thesis: b

then consider k being Nat such that

A2: x in A |^ k by FLANG_1:41;

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

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