let E be set ; :: thesis: for A being Subset of (E ^omega)
for m, n, k being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
let A be Subset of (E ^omega); :: thesis: for m, n, k being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
let m, n, k be Nat; :: thesis: (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))

per cases ( m <= n or k = 0 or ( m > n & k <> 0 ) ) ;

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

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

A2: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A3: m * k <= n * k by A1, XREAL_1:66;
assume S₁[k] ; :: thesis: S₁[k + 1]
then (A |^ (m,n)) |^ (k + 1) = (A |^ ((m * k),(n * k))) ^^ (A |^ (m,n)) by FLANG_1:24
.= A |^ (((m * k) + m),((n * k) + n)) by A1, A3, Th37
.= A |^ ((m * (k + 1)),(n * (k + 1))) ;
hence S₁[k + 1] ; :: thesis: verum

end;

(A |^ (m,n)) |^ 0 = {(<%> E)} by FLANG_1:25
.= A |^ 0 by FLANG_1:25
.= A |^ ((m * 0),(n * 0)) by Th22 ;
then A4: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A4, A2);
hence (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) ; :: thesis: verum

end;

suppose A5: k = 0 ; :: thesis: (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))

hence (A |^ (m,n)) |^ k = {(<%> E)} by FLANG_1:25
.= A |^ 0 by FLANG_1:25
.= A |^ ((m * k),(n * k)) by A5, Th22 ;
:: thesis: verum

end;

suppose A6: ( m > n & k <> 0 ) ; :: thesis: (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))

then A |^ (m,n) = {} by Th21;
then A7: (A |^ (m,n)) |^ k = {} by A6, FLANG_1:28;
m * k > n * k by A6, XREAL_1:70;
hence (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) by A7, Th21; :: thesis: verum

end;

end;