let E be set ; for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
let A be Subset of (E ^omega); for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
let k, m, n be Nat; (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
per cases
( m <= n or m > n )
;
suppose A1:
m <= n
;
(A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))defpred S1[
Nat]
means (A |^ $1) |^ (
m,
n)
c= A |^ (
($1 * m),
($1 * n));
A2:
now for l being Nat st S1[l] holds
S1[l + 1]let l be
Nat;
( S1[l] implies S1[l + 1] )A3:
l * m <= l * n
by A1, XREAL_1:64;
assume
S1[
l]
;
S1[l + 1]then A4:
((A |^ l) |^ (m,n)) ^^ ((A |^ 1) |^ (m,n)) c= (A |^ ((l * m),(l * n))) ^^ ((A |^ 1) |^ (m,n))
by FLANG_1:17;
(A |^ (l + 1)) |^ (
m,
n)
c= ((A |^ l) |^ (m,n)) ^^ (A |^ (m,n))
by Th41;
then A5:
(A |^ (l + 1)) |^ (
m,
n)
c= ((A |^ l) |^ (m,n)) ^^ ((A |^ 1) |^ (m,n))
by FLANG_1:25;
(A |^ ((l * m),(l * n))) ^^ ((A |^ 1) |^ (m,n)) =
(A |^ ((l * m),(l * n))) ^^ (A |^ (m,n))
by FLANG_1:25
.=
A |^ (
((l * m) + m),
((l * n) + n))
by A1, A3, Th37
.=
A |^ (
((l + 1) * m),
((l + 1) * n))
;
hence
S1[
l + 1]
by A5, A4, XBOOLE_1:1;
verum end; (A |^ 0) |^ (
m,
n) =
{(<%> E)} |^ (
m,
n)
by FLANG_1:24
.=
{(<%> E)}
by A1, Th31
.=
A |^ 0
by FLANG_1:24
.=
A |^ (
(0 * m),
(0 * n))
by Th22
;
then A6:
S1[
0 ]
;
for
l being
Nat holds
S1[
l]
from NAT_1:sch 2(A6, A2);
hence
(A |^ k) |^ (
m,
n)
c= A |^ (
(k * m),
(k * n))
;
verum end; end;