let E be set ; :: thesis: for A being Subset of (E ^omega)

for n being Nat holds (A |^.. n) * = (A |^.. n) ?

let A be Subset of (E ^omega); :: thesis: for n being Nat holds (A |^.. n) * = (A |^.. n) ?

let n be Nat; :: thesis: (A |^.. n) * = (A |^.. n) ?

(A |^.. n) ? c= (A |^.. n) * by FLANG_2:86;

hence (A |^.. n) * = (A |^.. n) ? by A5, XBOOLE_0:def 10; :: thesis: verum

for n being Nat holds (A |^.. n) * = (A |^.. n) ?

let A be Subset of (E ^omega); :: thesis: for n being Nat holds (A |^.. n) * = (A |^.. n) ?

let n be Nat; :: thesis: (A |^.. n) * = (A |^.. n) ?

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

x in (A |^.. n) ?

then A5:
(A |^.. n) * c= (A |^.. n) ?
;x in (A |^.. n) ?

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

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

then consider k being Nat such that

A1: x in (A |^.. n) |^ k by FLANG_1:41;

end;assume x in (A |^.. n) * ; :: thesis: b

then consider k being Nat such that

A1: x in (A |^.. n) |^ k by FLANG_1:41;

per cases
( k = 0 or k > 0 )
;

end;

suppose
k = 0
; :: thesis: b_{1} in (A |^.. n) ?

then
x in ((A |^.. n) |^ 0) \/ ((A |^.. n) |^ 1)
by A1, XBOOLE_0:def 3;

hence x in (A |^.. n) ? by FLANG_2:75; :: thesis: verum

end;hence x in (A |^.. n) ? by FLANG_2:75; :: thesis: verum

suppose A2:
k > 0
; :: thesis: b_{1} in (A |^.. n) ?

then
(A |^.. n) |^ k c= A |^.. (n * k)
by Th19;

then consider l being Nat such that

A3: n * k <= l and

A4: x in A |^ l by A1, Th2;

k >= 0 + 1 by A2, NAT_1:13;

then n * k >= n by XREAL_1:151;

then l >= n by A3, XXREAL_0:2;

then x in A |^.. n by A4, Th2;

then x in (A |^.. n) |^ 1 by FLANG_1:25;

then x in ((A |^.. n) |^ 0) \/ ((A |^.. n) |^ 1) by XBOOLE_0:def 3;

hence x in (A |^.. n) ? by FLANG_2:75; :: thesis: verum

end;then consider l being Nat such that

A3: n * k <= l and

A4: x in A |^ l by A1, Th2;

k >= 0 + 1 by A2, NAT_1:13;

then n * k >= n by XREAL_1:151;

then l >= n by A3, XXREAL_0:2;

then x in A |^.. n by A4, Th2;

then x in (A |^.. n) |^ 1 by FLANG_1:25;

then x in ((A |^.. n) |^ 0) \/ ((A |^.. n) |^ 1) by XBOOLE_0:def 3;

hence x in (A |^.. n) ? by FLANG_2:75; :: thesis: verum

(A |^.. n) ? c= (A |^.. n) * by FLANG_2:86;

hence (A |^.. n) * = (A |^.. n) ? by A5, XBOOLE_0:def 10; :: thesis: verum