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) ?

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

let x be object ; :: thesis: ( x in (A |^.. n) * implies b₁ in (A |^.. n) ? )
assume x in (A |^.. n) * ; :: thesis: b₁ in (A |^.. n) ?
then consider k being Nat such that
A1: x in (A |^.. n) |^ k by FLANG_1:41;

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

suppose k = 0 ; :: thesis: b₁ 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;

suppose A2: k > 0 ; :: thesis: b₁ 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;

end;

end;

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