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