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