let E be set ; for A being Subset of (E ^omega)
for m, n being Nat holds (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))
let A be Subset of (E ^omega); for m, n being Nat holds (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))
let m, n be Nat; (A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))
A1:
(A *) ^^ (A |^ (m,n)) c= (A |^ (m,n)) ^^ (A *)
proof
let x be
object ;
TARSKI:def 3 ( not x in (A *) ^^ (A |^ (m,n)) or x in (A |^ (m,n)) ^^ (A *) )
assume
x in (A *) ^^ (A |^ (m,n))
;
x in (A |^ (m,n)) ^^ (A *)
then consider a,
b being
Element of
E ^omega such that A2:
a in A *
and A3:
b in A |^ (
m,
n)
and A4:
x = a ^ b
by FLANG_1:def 1;
consider k being
Nat such that A5:
a in A |^ k
by A2, FLANG_1:41;
consider mn being
Nat such that A6:
(
m <= mn &
mn <= n )
and A7:
b in A |^ mn
by A3, Th19;
(
A |^ k c= A * &
A |^ mn c= A |^ (
m,
n) )
by A6, Th20, FLANG_1:42;
then A8:
(A |^ mn) ^^ (A |^ k) c= (A |^ (m,n)) ^^ (A *)
by FLANG_1:17;
a ^ b in A |^ (mn + k)
by A7, A5, FLANG_1:40;
then
a ^ b in (A |^ mn) ^^ (A |^ k)
by FLANG_1:33;
hence
x in (A |^ (m,n)) ^^ (A *)
by A4, A8;
verum
end;
(A |^ (m,n)) ^^ (A *) c= (A *) ^^ (A |^ (m,n))
proof
let x be
object ;
TARSKI:def 3 ( not x in (A |^ (m,n)) ^^ (A *) or x in (A *) ^^ (A |^ (m,n)) )
assume
x in (A |^ (m,n)) ^^ (A *)
;
x in (A *) ^^ (A |^ (m,n))
then consider a,
b being
Element of
E ^omega such that A9:
a in A |^ (
m,
n)
and A10:
b in A *
and A11:
x = a ^ b
by FLANG_1:def 1;
consider k being
Nat such that A12:
b in A |^ k
by A10, FLANG_1:41;
consider mn being
Nat such that A13:
(
m <= mn &
mn <= n )
and A14:
a in A |^ mn
by A9, Th19;
(
A |^ k c= A * &
A |^ mn c= A |^ (
m,
n) )
by A13, Th20, FLANG_1:42;
then A15:
(A |^ k) ^^ (A |^ mn) c= (A *) ^^ (A |^ (m,n))
by FLANG_1:17;
a ^ b in A |^ (k + mn)
by A14, A12, FLANG_1:40;
then
a ^ b in (A |^ k) ^^ (A |^ mn)
by FLANG_1:33;
hence
x in (A *) ^^ (A |^ (m,n))
by A11, A15;
verum
end;
hence
(A |^ (m,n)) ^^ (A *) = (A *) ^^ (A |^ (m,n))
by A1, XBOOLE_0:def 10; verum