let E be set ; :: thesis: for A being Subset of ()
for m, n being Nat st n > 0 holds
(A |^.. m) |^ n = A |^.. (m * n)

let A be Subset of (); :: thesis: for m, n being Nat st n > 0 holds
(A |^.. m) |^ n = A |^.. (m * n)

let m, n be Nat; :: thesis: ( n > 0 implies (A |^.. m) |^ n = A |^.. (m * n) )
defpred S1[ Nat] means ( \$1 > 0 implies (A |^.. m) |^ \$1 = A |^.. (m * \$1) );
A1: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
now :: thesis: ( n + 1 > 0 implies (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1)) )
assume n + 1 > 0 ; :: thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1))
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1))
hence (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1)) by FLANG_1:25; :: thesis: verum
end;
suppose n > 0 ; :: thesis: (A |^.. m) |^ (n + 1) = A |^.. (m * (n + 1))
hence (A |^.. m) |^ (n + 1) = (A |^.. (m * n)) ^^ (A |^.. m) by
.= A |^.. ((m * n) + m) by Th18
.= A |^.. (m * (n + 1)) ;
:: thesis: verum
end;
end;
end;
hence S1[n + 1] ; :: thesis: verum
end;
A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A1);
hence ( n > 0 implies (A |^.. m) |^ n = A |^.. (m * n) ) ; :: thesis: verum