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