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