let E be set ; :: thesis: for A being Subset of (E ^omega )
for n being Nat st <%> E in A holds
(A |^ n) * = (A * ) |^ n
let A be Subset of (E ^omega ); :: thesis: for n being Nat st <%> E in A holds
(A |^ n) * = (A * ) |^ n
let n be Nat; :: thesis: ( <%> E in A implies (A |^ n) * = (A * ) |^ n )
assume A1: <%> E in A ; :: thesis: (A |^ n) * = (A * ) |^ n

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

suppose A2: n = 0 ; :: thesis: (A |^ n) * = (A * ) |^ n

hence (A |^ n) * = {(<%> E)} * by FLANG_1:25
.= {(<%> E)} by FLANG_1:48
.= (A * ) |^ n by A2, FLANG_1:25 ;
:: thesis: verum

end;

suppose A3: n > 0 ; :: thesis: (A |^ n) * = (A * ) |^ n

then (A * ) |^ n = A * by FLANG_1:67;
hence (A |^ n) * = (A * ) |^ n by A1, A3, Th16; :: thesis: verum

end;

end;