let E be set ; :: thesis: for A being Subset of (E ^omega)
for n, m being Nat holds (A |^ m) |^ n = A |^ (m * n)
let A be Subset of (E ^omega); :: thesis: for n, m being Nat holds (A |^ m) |^ n = A |^ (m * n)
let n, m be Nat; :: thesis: (A |^ m) |^ n = A |^ (m * n)
defpred S1[ Nat] means for m, n being Nat st m + n <= $1 holds
(A |^ m) |^ n = A |^ (m * n);
A1: now :: thesis: for l being Nat st S1[l] holds
S1[l + 1]
let l be Nat; :: thesis: ( S1[l] implies S1[l + 1] )
assume A2: S1[l] ; :: thesis: S1[l + 1]
now :: thesis: for m, n being Nat st m + n <= l + 1 holds
(A |^ m) |^ n = A |^ (m * n)
let m, n be Nat; :: thesis: ( m + n <= l + 1 implies (A |^ m) |^ n = A |^ (m * n) )
A3: now :: thesis: ( m + n < l + 1 implies (A |^ m) |^ n = A |^ (m * n) )
assume m + n < l + 1 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
then m + n <= l by NAT_1:13;
hence (A |^ m) |^ n = A |^ (m * n) by A2; :: thesis: verum
end;
A4: now :: thesis: ( m + n = l + 1 implies (A |^ m) |^ n = A |^ (m * n) )
assume A5: m + n = l + 1 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
A6: now :: thesis: ( m > 0 & n > 0 implies (A |^ m) |^ n = A |^ (m * n) )
assume that
m > 0 and
A7: n > 0 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
consider k being Nat such that
A8: k + 1 = n by A7, NAT_1:6;
A9: m + k <= l by A5, A8;
(A |^ m) |^ n = ((A |^ m) |^ k) ^^ (A |^ m) by A8, Th23
.= (A |^ (m * k)) ^^ (A |^ m) by A2, A9
.= A |^ ((m * k) + m) by Th33
.= A |^ (m * n) by A8 ;
hence (A |^ m) |^ n = A |^ (m * n) ; :: thesis: verum
end;
A10: now :: thesis: ( n = 0 implies (A |^ m) |^ n = A |^ (m * n) )
assume A11: n = 0 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
hence (A |^ m) |^ n = {(<%> E)} by Th24
.= A |^ (m * n) by A11, Th24 ;
:: thesis: verum
end;
now :: thesis: ( m = 0 implies (A |^ m) |^ n = A |^ (m * n) )
assume A12: m = 0 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
hence (A |^ m) |^ n = {(<%> E)} |^ n by Th24
.= {(<%> E)} by Th28
.= A |^ (m * n) by A12, Th24 ;
:: thesis: verum
end;
hence (A |^ m) |^ n = A |^ (m * n) by A10, A6; :: thesis: verum
end;
assume m + n <= l + 1 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
hence (A |^ m) |^ n = A |^ (m * n) by A4, A3, XXREAL_0:1; :: thesis: verum
end;
hence S1[l + 1] ; :: thesis: verum
end;
A13: S1[ 0 ]
proof
let m, n be Nat; :: thesis: ( m + n <= 0 implies (A |^ m) |^ n = A |^ (m * n) )
assume A14: m + n <= 0 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
then A15: m = 0 ;
n = 0 by A14;
hence (A |^ m) |^ n = {(<%> E)} by Th24
.= A |^ (m * n) by A15, Th24 ;
:: thesis: verum
end;
A16: for l being Nat holds S1[l] from NAT_1:sch 2(A13, A1);
now :: thesis: for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n)
let m, n be Nat; :: thesis: (A |^ m) |^ n = A |^ (m * n)
reconsider l = m + n as Nat ;
m + n <= l ;
hence (A |^ m) |^ n = A |^ (m * n) by A16; :: thesis: verum
end;
hence (A |^ m) |^ n = A |^ (m * n) ; :: thesis: verum