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 object ; :: 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:34;
then x in A |^ ((k * mn) + (l * mn)) ;
then x in (A |^ (k * mn)) ^^ (A |^ (l * mn)) by FLANG_1:33;
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:34;
then A6: b in (A |^ l) |^ (m,n) by A1, Th19;
a in (A |^ k) |^ mn by A3, FLANG_1:34;
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