let E be set ; :: thesis: for A being Subset of (E ^omega)

for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n)

let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n)

let m, n be Nat; :: thesis: (A |^ m) |^.. n c= A |^.. (m * n)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^ m) |^.. n or x in A |^.. (m * n) )

assume x in (A |^ m) |^.. n ; :: thesis: x in A |^.. (m * n)

then consider k being Nat such that

A1: k >= n and

A2: x in (A |^ m) |^ k by Th2;

A3: m * k >= m * n by A1, XREAL_1:64;

x in A |^ (m * k) by A2, FLANG_1:34;

hence x in A |^.. (m * n) by A3, Th2; :: thesis: verum

for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n)

let A be Subset of (E ^omega); :: thesis: for m, n being Nat holds (A |^ m) |^.. n c= A |^.. (m * n)

let m, n be Nat; :: thesis: (A |^ m) |^.. n c= A |^.. (m * n)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A |^ m) |^.. n or x in A |^.. (m * n) )

assume x in (A |^ m) |^.. n ; :: thesis: x in A |^.. (m * n)

then consider k being Nat such that

A1: k >= n and

A2: x in (A |^ m) |^ k by Th2;

A3: m * k >= m * n by A1, XREAL_1:64;

x in A |^ (m * k) by A2, FLANG_1:34;

hence x in A |^.. (m * n) by A3, Th2; :: thesis: verum