let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A *
let A be Subset of (E ^omega); :: thesis: for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A *
let k, m, n be Nat; :: thesis: (A |^ k) |^ (m,n) c= A *
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^ k) |^ (m,n) or x in A * )
assume x in (A |^ k) |^ (m,n) ; :: thesis: x in A *
then consider mn being Nat such that
m <= mn and
mn <= n and
A1: x in (A |^ k) |^ mn by Th19;
A2: A |^ (k * mn) c= A * by FLANG_1:42;
x in A |^ (k * mn) by A1, FLANG_1:34;
hence x in A * by A2; :: thesis: verum