let E be set ; 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); for m, n being Nat holds (A |^ (m,n)) * c= A *
let m, n be Nat; (A |^ (m,n)) * c= A *
let x be object ; TARSKI:def 3 ( not x in (A |^ (m,n)) * or x in A * )
assume
x in (A |^ (m,n)) *
; x in A *
then consider k being Nat such that
A1:
x in (A |^ (m,n)) |^ k
by FLANG_1:41;
( (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) & A |^ ((m * k),(n * k)) c= A * )
by Th32, Th40;
hence
x in A *
by A1; verum