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

let x be set ; :: 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 set 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