let E be set ; for A being Subset of (E ^omega)
for k, l, m, n being Nat st m <= n & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
let A be Subset of (E ^omega); for k, l, m, n being Nat st m <= n & k <= l holds
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
let k, l, m, n be Nat; ( m <= n & k <= l implies (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l)) )
assume A1:
( m <= n & k <= l )
; (A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
A2:
now for x being object st x in A |^ ((m + k),(n + l)) holds
x in (A |^ (m,n)) ^^ (A |^ (k,l))let x be
object ;
( x in A |^ ((m + k),(n + l)) implies x in (A |^ (m,n)) ^^ (A |^ (k,l)) )assume
x in A |^ (
(m + k),
(n + l))
;
x in (A |^ (m,n)) ^^ (A |^ (k,l))then consider i being
Nat such that A3:
(
m + k <= i &
i <= n + l )
and A4:
x in A |^ i
by Th19;
consider mn,
kl being
Nat such that A5:
mn + kl = i
and A6:
(
m <= mn &
mn <= n &
k <= kl &
kl <= l )
by A1, A3, Th2;
(
A |^ mn c= A |^ (
m,
n) &
A |^ kl c= A |^ (
k,
l) )
by A6, Th20;
then
(A |^ mn) ^^ (A |^ kl) c= (A |^ (m,n)) ^^ (A |^ (k,l))
by FLANG_1:17;
then
A |^ (mn + kl) c= (A |^ (m,n)) ^^ (A |^ (k,l))
by FLANG_1:33;
hence
x in (A |^ (m,n)) ^^ (A |^ (k,l))
by A4, A5;
verum end;
now for x being object st x in (A |^ (m,n)) ^^ (A |^ (k,l)) holds
x in A |^ ((m + k),(n + l))let x be
object ;
( x in (A |^ (m,n)) ^^ (A |^ (k,l)) implies x in A |^ ((m + k),(n + l)) )assume
x in (A |^ (m,n)) ^^ (A |^ (k,l))
;
x in A |^ ((m + k),(n + l))then consider a,
b being
Element of
E ^omega such that A7:
a in A |^ (
m,
n)
and A8:
b in A |^ (
k,
l)
and A9:
x = a ^ b
by FLANG_1:def 1;
consider kl being
Nat such that A10:
k <= kl
and A11:
kl <= l
and A12:
b in A |^ kl
by A8, Th19;
consider mn being
Nat such that A13:
m <= mn
and A14:
mn <= n
and A15:
a in A |^ mn
by A7, Th19;
A16:
mn + kl <= n + l
by A14, A11, XREAL_1:7;
(
a ^ b in A |^ (mn + kl) &
m + k <= mn + kl )
by A13, A15, A10, A12, FLANG_1:40, XREAL_1:7;
hence
x in A |^ (
(m + k),
(n + l))
by A9, A16, Th19;
verum end;
hence
(A |^ (m,n)) ^^ (A |^ (k,l)) = A |^ ((m + k),(n + l))
by A2, TARSKI:2; verum