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: S₁[ 0 ]

proof

(A |^ 0 ) |^ m,n = {(<%> E)} |^ m,n by FLANG_1:25
.= {(<%> E)} by A1, Th31
.= A |^ 0 by FLANG_1:25
.= A |^ (0 * m),(0 * n) by Th22 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A3: now

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
A4: l * m <= l * n by A1, XREAL_1:66;
assume A5: S₁[l] ; :: thesis: S₁[l + 1]
(A |^ (l + 1)) |^ m,n c= ((A |^ l) |^ m,n) ^^ (A |^ m,n) by Th41;
then A6: (A |^ (l + 1)) |^ m,n c= ((A |^ l) |^ m,n) ^^ ((A |^ 1) |^ m,n) by FLANG_1:26;
A7: ((A |^ l) |^ m,n) ^^ ((A |^ 1) |^ m,n) c= (A |^ (l * m),(l * n)) ^^ ((A |^ 1) |^ m,n) by A5, FLANG_1:18;
(A |^ (l * m),(l * n)) ^^ ((A |^ 1) |^ m,n) = (A |^ (l * m),(l * n)) ^^ (A |^ m,n) by FLANG_1:26
.= A |^ ((l * m) + m),((l * n) + n) by A1, A4, Th37
.= A |^ ((l + 1) * m),((l + 1) * n) ;
hence S₁[l + 1] by A6, A7, XBOOLE_1:1; :: thesis: verum

end;

for l being Nat holds S₁[l] from NAT_1:sch 2(A2, A3);
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) by XBOOLE_1:2; :: thesis: verum

end;

end;