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

A2: now

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

now

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:26; :: 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 A3, FLANG_1:24
.= A |^.. ((m * n) + m) by Th18
.= A |^.. (m * (n + 1)) ;
:: thesis: verum

end;

end;

end;

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence ( n > 0 implies (A |^.. m) |^ n = A |^.. (m * n) ) ; :: thesis: verum