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

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[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 A2, FLANG_1:23
.= A |^.. ((m * n) + m) by Th18
.= A |^.. (m * (n + 1)) ;
:: thesis: verum

end;

end;

end;

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

end;

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