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
set ;
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:42;
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:43;
then A8:
(A |^ mn) ^^ (A |^ k) c= (A |^ m,n) ^^ (A * )
by FLANG_1:18;
a ^ b in A |^ (mn + k)
by A7, A5, FLANG_1:41;
then
a ^ b in (A |^ mn) ^^ (A |^ k)
by FLANG_1:34;
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
set ;
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:42;
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:43;
then A15:
(A |^ k) ^^ (A |^ mn) c= (A * ) ^^ (A |^ m,n)
by FLANG_1:18;
a ^ b in A |^ (k + mn)
by A14, A12, FLANG_1:41;
then
a ^ b in (A |^ k) ^^ (A |^ mn)
by FLANG_1:34;
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