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 b1 in (A |^.. n) ? )
assume x in (A |^.. n) * ; :: thesis: b1 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: b1 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: b1 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