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:24
.= {(<%> E)} by FLANG_1:47
.= (A *) |^ n by A2, FLANG_1:24 ;
:: thesis: verum
end;
suppose A3: n > 0 ; :: thesis: (A |^ n) * = (A *) |^ n
then (A *) |^ n = A * by FLANG_1:66;
hence (A |^ n) * = (A *) |^ n by A1, A3, Th16; :: thesis: verum
end;
end;