let E be set ; :: thesis: for A being Subset of (E ^omega)
for k, m, n being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
let A be Subset of (E ^omega); :: thesis: for k, m, n being Nat holds (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k))
let k, m, n 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 S1[ Nat] means (A |^ (m,n)) |^ $1 = A |^ ((m * $1),(n * $1));
A2: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A3: m * k <= n * k by A1, XREAL_1:64;
assume S1[k] ; :: thesis: S1[k + 1]
then (A |^ (m,n)) |^ (k + 1) = (A |^ ((m * k),(n * k))) ^^ (A |^ (m,n)) by FLANG_1:23
.= A |^ (((m * k) + m),((n * k) + n)) by A1, A3, Th37
.= A |^ ((m * (k + 1)),(n * (k + 1))) ;
hence S1[k + 1] ; :: thesis: verum
end;
(A |^ (m,n)) |^ 0 = {(<%> E)} by FLANG_1:24
.= A |^ 0 by FLANG_1:24
.= A |^ ((m * 0),(n * 0)) by Th22 ;
then A4: S1[ 0 ] ;
for k being Nat holds S1[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:24
.= A |^ 0 by FLANG_1:24
.= 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:27;
m * k > n * k by A6, XREAL_1:68;
hence (A |^ (m,n)) |^ k = A |^ ((m * k),(n * k)) by A7, Th21; :: thesis: verum
end;
end;