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

A1: now :: thesis: for x being object st x in A |^ (m,m) holds
x in A |^ m

let x be object ; :: thesis: ( x in A |^ (m,m) implies x in A |^ m )
assume x in A |^ (m,m) ; :: thesis: x in A |^ m
then ex k being Nat st
( m <= k & k <= m & x in A |^ k ) by Th19;
hence x in A |^ m by XXREAL_0:1; :: thesis: verum

end;

for x being object st x in A |^ m holds
x in A |^ (m,m) by Th19;
hence A |^ (m,m) = A |^ m by A1, TARSKI:2; :: thesis: verum