let E be set ; :: thesis: for A being Subset of (E ^omega )
for m, n being Nat holds (A |^ m) |^ n = A |^ (m * n)
let A be Subset of (E ^omega ); :: 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)
defpred S₁[ Nat] means for m, n being Nat st m + n <= $1 holds
(A |^ m) |^ n = A |^ (m * n);
A1: S₁[ 0 ]

proof

let m, n be Nat; :: thesis: ( m + n <= 0 implies (A |^ m) |^ n = A |^ (m * n) )
assume m + n <= 0 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
then m + n = 0 ;
then A2: ( m = 0 & n = 0 ) ;
hence (A |^ m) |^ n = {(<%> E)} by Th25
.= A |^ (m * n) by A2, Th25 ;
:: thesis: verum

end;

A3: now

let l be Nat; :: thesis: ( S₁[l] implies S₁[l + 1] )
assume A4: S₁[l] ; :: thesis: S₁[l + 1]

now

let m, n be Nat; :: 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

assume A7: m + n = l + 1 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)

A8: now

assume A9: m = 0 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
hence (A |^ m) |^ n = {(<%> E)} |^ n by Th25
.= {(<%> E)} by Th29
.= A |^ (m * n) by A9, Th25 ;
:: thesis: verum

end;

A10: now

assume A11: n = 0 ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
hence (A |^ m) |^ n = {(<%> E)} by Th25
.= A |^ (m * n) by A11, Th25 ;
:: thesis: verum

end;

now

assume ( m > 0 & n > 0 ) ; :: thesis: (A |^ m) |^ n = A |^ (m * n)
then consider k being Nat such that
A12: k + 1 = n by NAT_1:6;
A13: m + k <= l by A7, A12;
(A |^ m) |^ n = ((A |^ m) |^ k) ^^ (A |^ m) by A12, Th24
.= (A |^ (m * k)) ^^ (A |^ m) by A4, A13
.= A |^ ((m * k) + m) by Th34
.= A |^ (m * n) by A12 ;
hence (A |^ m) |^ n = A |^ (m * n) ; :: thesis: verum

end;

hence (A |^ m) |^ n = A |^ (m * n) by A8, A10; :: thesis: verum

end;

now

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 A4; :: thesis: verum

end;

hence (A |^ m) |^ n = A |^ (m * n) by A5, A6, XXREAL_0:1; :: thesis: verum

end;

hence S₁[l + 1] ; :: thesis: verum

end;

A14: for l being Nat holds S₁[l] from NAT_1:sch 2(A1, A3);

now

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 A14; :: thesis: verum

end;

hence (A |^ m) |^ n = A |^ (m * n) ; :: thesis: verum