let E be set ; :: thesis: 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); :: thesis: for k, m, n being Nat holds (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))
let k, m, n be Nat; :: thesis: (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))

per cases ( m <= n or m > n ) ;

suppose A1: m <= n ; :: thesis: (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))

defpred S₁[ Nat] means (A |^ $1) |^ (m,n) c= A |^ (($1 * m),($1 * n));

A2: now :: thesis: for l being Nat st S₁[l] holds
S₁[l + 1]

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
A3: l * m <= l * n by A1, XREAL_1:64;
assume S₁[l] ; :: thesis: S₁[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 S₁[l + 1] by A5, A4, XBOOLE_1:1; :: thesis: 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: S₁[ 0 ] ;
for l being Nat holds S₁[l] from NAT_1:sch 2(A6, A2);
hence (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n)) ; :: thesis: verum

end;

suppose m > n ; :: thesis: (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n))

then (A |^ k) |^ (m,n) = {} by Th21;
hence (A |^ k) |^ (m,n) c= A |^ ((k * m),(k * n)) ; :: thesis: verum

end;

end;