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 object ; :: 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:17;
x in A |^ ((k + 1) * mn) by A2, FLANG_1:34;
then x in A |^ ((k * mn) + mn) ;
then x in (A |^ (k * mn)) ^^ (A |^ mn) by FLANG_1:33;
then A4: x in ((A |^ k) |^ mn) ^^ (A |^ mn) by FLANG_1:34;
(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:17;
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