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