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

proof

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

end;

A3: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A4: 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, A4, Th37
.= A |^ (m * (k + 1)),(n * (k + 1)) ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
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 A7: k > 0 ;
A |^ m,n = {} by A6, Th21;
then A8: (A |^ m,n) |^ k = {} by A7, FLANG_1:28;
m * k > n * k by A6, XREAL_1:70;
hence (A |^ m,n) |^ k = A |^ (m * k),(n * k) by A8, Th21; :: thesis: verum

end;

end;